Release of Coq 8.13.0

Dear Coq users,

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

The full list of changes is available at the following address

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