This example stopped working for me:
http://github.com/mattam82/Coq-Equations/raw/master/doc/equations_intro.v
Equations head {A} (l : list A) (pf : l <> nil) : A :=
head nil pf with (pf eq_refl) := { | x :=! x };
head (cons a v) _ := a.
Error: Illegal application (Non-functional construction):
The expression "!" of type "equations_tag" cannot be applied to the term
"x" : "False"
IIRC, the idiomatic way is now { | ! }
instead of { | x :=! x }
@Matthieu Sozeau Thanks. That works. Please consider updating the file.
Last updated: Dec 07 2023 at 07:39 UTC