Skip to content

Coq 8.13+beta1

Pre-release
Pre-release
Compare
Choose a tag to compare
@gares gares released this 07 Dec 14:52
· 119 commits to v8.13 since this release
V8.13+beta1
This tag was signed with the committer’s verified signature.
gares Enrico Tassi
GPG key ID: 250533CCA29B764F
Learn about vigilant mode.
5f7bf8d
This commit was signed with the committer’s verified signature.
gares Enrico Tassi
GPG key ID: 250533CCA29B764F
Learn about vigilant mode.

We encourage our users to test this beta release, in particular:

  • The windows installer is now based on the Coq platform: This
    greatly simplifies its build process and makes it easy to add
    more packages. At the same time this new installer was only
    tested by two people, so if you use Windows please give us
    feedback on any problem you may encounter.

  • The notation system received many fixes and improvements, in
    particular the way notations are selected for printing changed:
    Coq now prefers notations which match a larger part of the term to
    abbreviate, and takes into account the order in which notations are
    imported in the current scope only in a second instance.
    The new rules were designed together with power users, and tested
    by some of them, but our automatic testing infrastructure for
    regressions in notation printing is still weak. If your Coq library
    makes heavy use of notations, please give us feedback on any
    regression.

See the changelog for the complete list of changes.

Assets 5