The Coq mailing list

[Yves Bertot <yves.bertot AT inria.fr>]

This is a correction:

- Since this release is a beta release, opam packages should not be in the coq released repository.  They have been moved to the coq extra-dev repository.  The proper approach to see the opam package is to do the following:

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install coq-mathcomp-character.1.11.0+beta1

(for instance)

- docker images are available as mathcomp/mathcomp:1.11.0-coq-dev, mathcomp/mathcomp:1.11.0-coq-8.11, etc...

On 4/16/20 4:06 PM, Yves Bertot wrote:

We are proud to announce the immediate availability of the Mathematical Components library version 1.11.0+beta1.

This release is compatible with Coq revisions from 8.7 to 8.11.

The main improvement introduced by this release is the introduction of
order structures. The change should be mostly visible by users of ssrnum. This is a beta release,
please report any issue to be fixed in the final release (planned in less than 6 weeks).

The contributors to this version are: Antonio Nikishaev, Anton Trunov, Assia Mahboubi, Cyril Cohen,
Enrico Tassi, Erik Martin-Dorel, Florent Hivert, Kazuhiko Sakaguchi, Pierre-Marie Pédrot,
Pierre-Yves Strub, Reynald Affeldt, Simon Boulier, Yves Bertot.

See https://github.com/math-comp/math-comp/releases/tag/mathcomp-1.11.0+beta1 to download and the file
CHANGELOG.md at https://github.com/math-comp/math-comp/blob/master/CHANGELOG.md to learn about new features.

Opam packages are also ready in the coq-released opam repository.

Best regards,
--
The Mathematical Components team