Skip to content

Equations v1.2.1 for Coq 8.9

Compare
Choose a tag to compare
@mattam82 mattam82 released this 05 Nov 19:45

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).