Release 1.2.1 of Equations is available, as source and
for Coq 8.9 and Coq 8.10.
The 8.10 version (only) includes support for the HoTT library (currently available
extra-dev repository only as
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
hoqc, one needs to pass the following additional
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.
– Matthieu Sozeau