The Coq mailing list

[Enrico Tassi <Enrico.Tassi AT inria.fr>]

Dear Coq users,

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

https://github.com/coq/coq/releases/tag/V8.13.0

The full list of changes is available at the following address

https://coq.github.io/doc/v8.13/refman/changes.html#version-8-13

      
Highlights:
- 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.

Best,
-- 
Enrico Tassi