`cofix` tactic without a name is deprecated
Closed this issue · 1 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 entry:
src/FormTopC/NatInfty.v:182:generalize dependent n. cofix.
ppedrot commented
This bug should be closed.