Release of Coq 8.13+beta1

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

The 8.13.0 release is expected to occur about one month from now.

1 Like