Coq 8.13+beta1 is out
Submitted by Enrico Tassi on December 7th, 2020
The Coq development team is proud to announce the immediate availability of Coq 8.13+beta1
Here the full list of changes.
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.