Dear Coq users,
The Coq development team is proud to announce the immediate
availability of Coq 8.13+beta1:
The full list of changes is available at the following address
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.
The 8.13.0 release is expected to occur about one month from now.