`cofix` tactic without a name is deprecated.
ejgallego opened this issue · 0 comments
ejgallego commented
The tactic form cofix. without a name is deprecated as it depends on the name of the current lemma.
See coq/coq#7196.
The backwards compatible fix is to use cofix name_of_the_fixpoint. Problematic entries in CoRN:
metric2/Limit.v:330: cofix.
metric2/Limit.v:344: cofix.
metric2/Limit.v:357: cofix.
reals/fast/CRseries.v:45: cofix.
reals/fast/CRseries.v:75: cofix.
reals/fast/CRseries.v:117: cofix.
reals/fast/CRseries.v:164: cofix.
reals/fast/CRseries.v:193: cofix.
reals/fast/CRseries.v:218: cofix.
reals/fast/CRseries.v:239: cofix.
reals/fast/CRseries.v:338: cofix.
reals/fast/CRseries.v:387: cofix.
reals/fast/CRseries.v:497: cofix.
reals/fast/CRseries.v:518: cofix.