Equations 1.2.2 for Coq 8.12
This is a bugfix release of version 1.2 working with Coq 8.12 (beta1 for now).
The bug fixes in the depind
and depelim
are potential sources of incompatibility.
See https://mattam82.github.io/Coq-Equations/equations/2019/05/17/1.2.html for the 1.2 release notes.
New in this version:
- Fixed issue #286 : allow let-ins in constructors
- Fixed issue #246: derive subterm for inductives with non-uniform parameters. Also force the user to derive
NoConfusion
beforeSubterm
, as required for the well-foundedness proof of the Subterm relation. Report an error when the user tries to derive the subterm relation on propositional inductive types (this is impossible). - PR #285: depelim and noconf were not working up-to simplification of equations. Potential source of incompatibility
- PR #283: depelim and depind no longer simplify unrelated equations in the goal (this was making some subgoals unprovable in some cases). Potential source of incompatibility
- PR #281: add an example of the
inspect
pattern in the documentation (by Yves Bertot). - Fixed issue #256: derive eliminators of well-founded definitions in presence of lets in the body.
- Fixed issue #273: derivation of the eliminator was launched too eagerly depending on the order the obligations of a definition were solved.
- Fixed deprecations in OCaml and .v files w.r.t. Coq 8.12