MathComp 1.12.0 released

We are proud to announce the immediate availability of the Mathematical
Components library version 1.12.0.
The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.10, Coq 8.11, and Coq 8.12.

The main changes are:

support for Coq 8.7, 8.8, and 8.9 have been dropped,
a change of implementation of intervals and the updated theory,
the addition of kernel lemmas for matrices,
generalized many lemmas for path and sorted,
several lemma additions, name changes and bug fixes.
The contributors to this version are: Anton Trunov, Christian Doczkal,
Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Jasper Hugunin, Kazuhiko
Sakaguchi, Laurent Théry, Reynald Affeldt, and Yves Bertot.
We also wish to thank all the reviewers of the various contributions.

See https://github.com/math-comp/math-comp/releases/tag/mathcomp-1.12.0
to download or see the CHANGELOG.md.

Packages for opam, nix, and docker are in preparation.

Best regards,
The Mathematical Components team

2 Likes