Dear Coq/Equations users, I’m happy to announce version 1.3 beta of the Equations package.
This is a new major release of Equations, working with Coq 8.13. This version adds an improved syntax (less ;
separation), integration with the CoqHoTT library and numerous bug fixes. See the reference manual for details.
This version introduces some minor potentially breaking changes along with the following features:

Improved syntax for “concise” clauses separated by

, at toplevel or insidewith
subprograms.
We no longer require to separate them by;
. For example, the following definition is now accepted:Equations foo : nat > nat :=  0 => 1  S n => S (foo n).
The old syntax is however still supported for backwards compatibility.

Require Import Equations.Equations.
does not work anymore.
One has to useRequire Import Equations.Prop.Equations
to load the plugin’s default instance where equality is inProp
.From Equations Require Import Equations
is unaffected. 
Use
Require Import Equations.HoTT.All
to use the HoTT variant of the library compatible with the Coq HoTT library
The plugin then reuses the definition ofpaths
from the HoTT library and all its constructions are universe polymorphic. As for the HoTT library alone, coq must be passed the argumentsnoinit indicesmatter
to use the library and plugin. Thecoqequations
opam package depends optionally oncoqhott
, so ifcoqhott
is installed before it,coqequations
will automatically install theHoTT
library variant in addition to the standard one.
The HoTT variant allows for example to patternmatch on equality proofs in the most concise way, e.g.:Require Import Equations.HoTT.All. Set Universe Polymorphism. Equations sym {A x y} (e : x = y :> A) : y = x := sym 1 => 1.

Multiple patterns can be separated by
,
in addition to
, as in:Equations trans {A} {x y z : A} (e : x = y) (e' : y = z) : x = z :=  1, 1 => 1.

New attribute
#[tactic=tac]
to set locally the default tactic to solve remaining holes.
The goals on which the tactic applies are now always of the formΓ  τ
where Γ is the context where the hole was introduced and τ the expected type, even when using theObligation
machinery to solve them, resulting in a possible incompatibility if the obligation tactic treated the context differently than the conclusion. By default, theprogram_simpl
tactic performs asimpl
call before introducing the hypotheses, so you might need to add asimpl in *
to your tactics. 
New attributes
#[derive(equations=yesno, eliminator=yesno)]
can be used in place of the(noeqns, noind)
flags which are deprecated.
Fixed in this version:
∗ #329: improved strengthening avoiding to abstract over recursive definitions which would not pass the guardness checker. This can simplify the produced terms, avoiding unnecessary “commutative cuts”.
∗ #321: warn rather than error when using Equations? and no subgoals are left. This will leave a proof state with no subgoals, that must be closed using a Qed
or Defined
(similarly to Coq’s #[refine] Instance
command).
∗ #372, #194: funelim
applied to a partial application failing
∗ #354: support for building values in SProp
∗ #353: name capture problem in presence of modules
∗ #335: provide an alias Equations Derive to not conflict with QuickChick’s Derive
∗ #325: properly inline all Equations helper constants during Extraction