Equations v1.2.1 for Coq 8.9

This is mainly a bugfix release of v1.2 including:

• Fixing the global export of Set Keyed Unification that broke users developments.
• Fix an undeclared universe anomaly in principle generation code.

Note: only Equations for Coq version 8.10 and above supports the use of the HoTT library (it required changes in both Coq and the HoTT library).

Equations v1.2.1 for Coq 8.10

This is mainly a bugfix release of v1.2 including:

• A version of the plugin working with the HoTT library
• Fixing the global export of Set Keyed Unification that broke users developments.
• Fix an undeclared universe anomaly in principle generation code.

Equations v1.2 for Coq 8.9

This final version contains mainly bugfixes over 1.2beta2, see announcement for more details

Equations v1.2 for Coq 8.8

This final version contains mainly bugfixes over 1.2beta2, see announcement for more details

Equations v1.2 for Coq 8.10

This final version contains mainly bugfixes over 1.2beta2, see announcement for more details.
It has been tested with the 8.10beta1 release of Coq.

Equations v1.2-beta2 for Coq 8.9

Bugfixes and new features, see announcement for more details

Equations v1.2-beta2 for Coq 8.8

Bugfixes and new features, see announcement for more details

Equations v1.2-beta for Coq 8.9

Release 1.2beta of Coq-Equations, see announcement here:

http://mattam82.github.io/Coq-Equations/equations/2019/01/28/1.2beta.html

Equations v1.2-beta for Coq 8.8

Release 1.2beta of Coq-Equations, see announcement here:

http://mattam82.github.io/Coq-Equations/equations/2019/01/28/1.2beta.html

Equations 1.1 for Coq 8.8

This is a bugfix release including many improvements to the treatment of nested recursive definitions, elimination principle generation, inaccessible patterns and proof automation tactics.