I am happy to announce availability of equations 1.2.4, a bugfix release that improves the compatibility of equations with ssreflect’s tactics and has more robust automated proofs of the elimination principle associated to a definition, including when functional extensionality is disabled. This version is available on opam for Coq 8.13, 8.12 and 8.11 and should be entirely backwards compatible.
Please report any issues at Issues · mattam82/Coq-Equations · GitHub
Matthieu Sozeau