coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] MathComp 1.9.0 released

From: georges gonthier <georges.gonthier AT inria.fr>
To: coq-club AT inria.fr, ssreflect AT msr-inria.inria.fr
Subject: [Coq-Club] MathComp 1.9.0 released
Date: Wed, 22 May 2019 16:11:40 +0200

We are proud to announce the immediate availability of the Mathematical Components library version 1.9.0.

This release is compatible with Coq 8.7, 8.8, 8.9 and 8.10beta1.

Future minor release will maintain compatibility with Coq 8.9 and 8.10, but may drop support for earlier versions.

The main changes are forward compatibility with Coq 8.10, including the {pred T} type and the nonPropType interface,

and refactoring of the seq.v theory of permutations, using a new deprecate notation to make backward compatible renamings.

The contributors to this version are: Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Georges Gonthier, Kazuhiko Sakaguchi, Sora Chen, Søren Eller Thomsen.

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

Best regards,

—

The Mathematical Components team

[Coq-Club] MathComp 1.9.0 released, georges gonthier, 05/22/2019