We are proud to announce the immediate availability of the Mathematical
Components library version 1.13.0.
The webpage, and documentation, are available at
https://math-comp.github.io/.
This release is compatible with Coq 8.11, 8.12, 8.13 and 8.14.
The main changes are new theories on the diagonalization of matrices,
on bounded sequences, and on the pairwise predicate.
The contributors to this version are: Amel Kebbouche, Anders Mörtberg,
Anton Trunov, Christian Doczkal, Cyril Cohen, Emilio Jesus Gallego
Arias, Enrico Tassi, Erik Martin-Dorel, Evgenii Moiseenko, Florent
Hivert, Gaëtan Gilbert, Kazuhiko Sakaguchi, Laurent Théry, Maxime
Dénès, Pierre Jouvelot, Pierre Roux, Reynald Affeldt, and Yves Bertot.
We also wish to thank all the reviewers of the various contributions.
See Release The Mathematical Components Library 1.13.0 · math-comp/math-comp · GitHub
to download or see the `CHANGELOG.md`.
Packages for opam, nix, and docker are in preparation.
Best regards,