Skip to content

Equations 1.2.4 for Coq 8.13
Compare
Choose a tag to compare
@mattam82 mattam82 released this 16 Mar 22:03
· 132 commits to 8.13 since this release
v1.2.4-8.13
99cb0f0

This is a bugfix release of version 1.2 working with Coq 8.13, 8.12 and 8.11
See https://mattam82.github.io/Coq-Equations/equations/2019/05/17/1.2.html for the 1.2 release notes.
Fixed in this version:

  • Fixed issues #228, #306 and #349 where functional elimination proofs were failing for no good reason. The tactic is now more robust and proves more unfolding lemmas without relying on functional extensionality (e.g. when no higher-order recursion is involved). It also generates smaller proof terms.
  • Fix conflicting grammar extension that declared "-!" as a token, conflicting with with ssr's rewrite syntax in particular. Now Equations also defines its potentially conflicting notations (for patterns, sigma-times etc) in an EquationsNotations module that does not have to be imported to make the plugin work (however the default is still to export them when Require Import Equations for compatibility and ease of use).
  • Fix issue #346: Derive not working when the inductive type's sort is hidden under a constant.
Assets 2
Loading