The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT inria.fr>]

We are proud to announce the immediate availability of:
- the Ssreflect proof language version 1.5 for Coq 8.4
- the Mathematical Components library version 1.5 for Coq 8.4

With this release "ssreflect" has been split into two packages.
The Ssreflect one contains the proof language (plugin for Coq) and a small set
of core theory libraries about boolean, natural numbers, sequences, decidable
equality  and finite types. The Mathematical Components one contains advanced
theory files covering a wider spectrum of mathematics.

With respect to version 1.4 the proof language got a few new features
related to forward reasoning and some bugfixes. The Mathematical Components
library features 16 new theory files and in particular: some field and Galois
theory, advanced character theory and a construction of algebraic numbers.

The new tarballs can be download at the following URLs:
  http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.tar.gz
  http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.tar.gz

The Ssreflect proof language user manual has been updated (see the
Changes section):
  http://hal.inria.fr/inria-00258384

The html documentation of the theory files can be browsed at:
  http://ssr.msr-inria.inria.fr/doc/ssreflect-1.5/
  http://ssr.msr-inria.inria.fr/doc/mathcomp-1.5/

-- The Mathematical Components team