Release 1.3beta2 of Equations is available, as source and through
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
dependent elimination and
funelim tactics for more robust proof scripts.
– Matthieu Sozeau