Skip to content

`fix` tactic without a name is deprecated.

The tactic form fix N where N is a number is deprecated as it depends on the name of the current lemma.

See https://github.com/coq/coq/pull/7196.

The backwards compatible fix is to use fix name_of_the_fixpoint N.

Edited by Ghost User