cv_termination_tac
cv_transLib.cv_termination_tac : tactic
A tactic for simplifying goals concerning cv_depth_sum.
This tactic is used by cv_transLib.cv_trans (and siblings) when
attempting to prove termination goals of translated :cv functions.
See also
cv_transLib.cv_trans,
cv_transLib.cv_trans_pre,
cv_transLib.cv_trans_pre_rec,
cv_transLib.cv_trans_rec,
cv_transLib.cv_auto_trans,
cv_transLib.cv_auto_trans_pre,
cv_transLib.cv_auto_trans_pre_rec,
cv_transLib.cv_auto_trans_rec,
cv_transLib.cv_eval