Release 1.2.1 of Equations is available, as source and through opam packages coq-equations.1.2.1+8.9, coq-equations.1.2.1+8.10 for Coq 8.9 and Coq 8.10.

The 8.10 version (only) includes support for the HoTT library (currently available in Coq’s extra-dev repository only as coq-hott-8.10.dev). Install coq-hott before Equations to get a version that uses the HoTT library. Note that only one of the HoTT variant or the standard variant can be installed at any given time. Using hoqtop or hoqc, one needs to pass the following additional options:

hoqtop/hoqc -I `coqc -where`/user-contrib/Equations -Q `coqc -where`/user-contrib ""

Then, one can import the plugin in Coq, using:

From Equations Require Import HoTT.All.

See the Reference Manual for an introduction to Equations, or the ICFP paper.

– Matthieu Sozeau