Equations 1.2 is released!
Release 1.2 of Equations is available, as source and
through opam
packages coqequations.1.2+8.8
,
coqequations.1.2+8.9
, coqequations.1.2+8.10
for Coq 8.8 and Coq
8.9 and Coq 8.10beta1 (the later in the extradev
repository).
I am pleased to announce release 1.2 of the Equations package. Equations is a function definition plugin for Coq, that supports the definition of functions by dependent patternmatching and structural or wellfounded, mutual or nested recursion and compiles them into core Coq terms without axioms. It automatically derives the clauses’ equations, the graph of the function and its associated elimination principle.
This release contains a few fixes and improvements with respect to the 1.2beta2 version:

Fixed an annoying backtracking bug when using
Equations?
(issue #179, thanks to PierreMarie Pédrot for help fixing this). 
Fixed the treatment of
with
with more than 2 arguments (issue #190) 
Fixed “cannot be used as a hint” errors (issue #193), now turned into warnings.

Granted with #187: global
Set Equations Derive Equations/Eliminator
options.
The previous beta1 and beta2 announcements describe the new features of the 1.2 version. See the reference manual for uptodate syntax and description of the new features. The Equations Reloaded paper also provides an introduction to the new version.
– Matthieu Sozeau