Release 1.3beta2 of Equations is available, as source and through opam package coq-equations.1.3~beta2+8.13, for Coq 8.13. See the release notes and updated reference manual for details. This beta version cleans up the interpretation of patterns and allow better preservation of user-given names by the dependent elimination and funelim tactics for more robust proof scripts.

– Matthieu Sozeau