v1.4.0

This release is compatible with math-comp 2.0.0 to 2.2.0 (and probably 2.3.0) on Coq 8.16 to 8.20

This is the first release where a separate directory is provided to describe solely the real numbers, together with a separate opam description.

v1.3.1

This release is compatible with math-comp 2.0.0 and 2.1.0 on Coq 8.16 to 8.18

v1.3.0

This release is compatible with math-comp 2.0.0 and Coq 8.16 to 8.17

v1.2.5

This release is compatible with math-comp 1.12 to 1.15 and Coq 8.11 to 8.16

v1.2.4

This release is compatible with math-comp 1.11 to 1.14

v1.2.3

This release is compatible with math-comp1.12

v1.2.2

This release is compatible with math-comp 1.11

v1.2.1

This release is compatible with math-comp 1.10.0

MathComp baseline

This is the first release of the Four Colour Theorem proof that is rebased on the SSReflect plugin and the MathComp library. The release number accounts for two much older releases:

• v1.0 for the initial 2005 release of the Coq v7.3 proof, which implemented the precursor to SSReflect using extensible grammars.
• v1.1 for the 2006 baseline release for the Mathematical Components project, which included the first native SSReflect implementation for Coq v8.0 and a few core files of the future MathComp library.
  While there were no public releases of the proof since, it had been regularly updated to track the evolution of Coq and SSReflect. This release takes advantage of the improvements in both the SSReflect proof language and the MathComp library, updates the proof style to the modern standards that have evolved from the MathComp development, and also substantially extends the internal documentation of the proof.