Coq 8.13.0 is out

The Coq development team is proud to announce the immediate availability of Coq 8.13.0


  • Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays.
  • Introduction of definitional proof irrelevance for the equality type defined in the SProp sort.
  • Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior.

Please see the changelog to learn more about this release.