Release 1.3 of Equations is available, as source and through opam packages for Coq 8.13, 8.14 and 8.15. See the release notes and updated reference manual for details. This new major version cleans up the input syntax (allowing to use less “;”), makes the interpretation of patterns more robust (disallowing dangerous shadowings) and better preserves user-given names by the dependent elimination and funelim tactics for more robust proof scripts.

– Matthieu Sozeau