Math Comp Versions Save

This release is compatible with Coq 8.11, 8.12, 8.13 and 8.14.

The main additions are:

• the theory of diagonalization of matrices,
• the pairwise predicate and its theory,
• bounded sequences and their theory,
• several lemmas in various parts of the library (order.v, finset.v, etc).

See the CHANGELOG.md file for more details.

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

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.

See the CHANGELOG.md file for more details.

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

The main change is a bug fix of 1.11+beta1 so that min and max work again on a partial order instead of a total order.

See the CHANGELOG.md file for more details.

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

The main improvement introduced by this release is the introduction of order structures. The change should mostly be visible by users of ssrnum.

This is a beta-release, please report any issues before the final release planned in less than 6 weeks.

See the CHANGELOG.md file for more details.

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

See the CHANGELOG.md file for more details.

This release is compatible with Coq 8.7, 8.8, 8.9 and 8.10beta1. Future minor releases will remain compatible with Coq 8.9 and 8.10; compatibility with earlier versions may be dropped.

See the CHANGELOG.md file for more details.

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

See the CHANGELOG.md file for more details.

This tags is for the first commit on github. The attached artifacts are the tarballs released before that.

Mar 18  2008 ssreflect-1.1.tgz
Aug 14  2009 ssreflect-1.2.tgz
Mar 25  2011 ssreflect-1.3pl1.tar.gz
Nov 21  2011 ssreflect-1.3pl2.tar.gz
May 14  2012 ssreflect-1.3pl3.tar.gz
May 14  2012 ssreflect-1.3pl4.tar.gz
Mar 11  2011 ssreflect-1.3.tar.gz
Sep  3  2012 ssreflect-1.4-coq8.3pl4-rc.tar.gz
Sep  5  2012 ssreflect-1.4-coq8.3pl4.tar.gz
Sep  3  2012 ssreflect-1.4-coq8.4-rc.tar.gz
Sep  5  2012 ssreflect-1.4-coq8.4.tar.gz
Sep  5  2012 ssreflect-1.4-doc.tar.gz
Jan 15  2015 ssreflect-1.5.coq85beta1.tar.gz
Jan 15  2015 mathcomp-1.5.coq85beta1.tar.gz
Apr 20  2015 ssreflect-1.5.coq85beta2.tar.gz
Apr 20  2015 mathcomp-1.5.coq85beta2.tar.gz
Aug  5  2013 ssreflect-1.5rc1.tar.gz
Aug  5  2013 mathcomp-1.5rc1.tar.gz
Mar 11  2014 ssreflect-1.5.tar.gz
Mar 11  2014 mathcomp-1.5.tar.gz

This release is compatible with Coq 8.6, 8.7 and 8.8. Windows installers available for Coq 8.8.0.

The main changes are a refactoring of algC and ssrnum, which led to generalizations and renamings. In the rest of the library a few theorems were added, generalized and/or renamed. See the ChangeLog file for more details.

This minor release:

• fixes a few issues of the build system under Windows
• removes compatibility with Coq 8.4.*; supported Coq versions are 8.5, 8.6 and 8.7