Skip to content

Equations 1.2.3 for Coq 8.11
Compare
Choose a tag to compare
@mattam82 mattam82 released this 30 Jul 11:29
· 18 commits to 8.11 since this release
v1.2.3-8.11
a524cdf
This commit was signed with the committer’s verified signature.
mattam82 Matthieu Sozeau
GPG key ID: 5560E767972A4459
Verified
Learn about vigilant mode.

This is a bugfix release of version 1.2 working with Coq 8.11
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 #297: dependent elimination simplification mistreated let-bindings
  • Fixed issue #295: discrepancy between the syntax in the manual and the implementation
  • Ensure that NoConfusion is derived before EqDec as it is necessary to solve the corresponding obligation.
Assets 2
Loading