Gaia release for MathComp 2.2.0

This release is known to work with Coq 8.16 to 8.20 and MathComp 2.0.0 to 2.2.0.

Gaia release for MathComp 2.0.0

This release is known to work with Coq 8.16 to 8.18 and MathComp 2.0.0. The main change is a port to MathComp 2 by Pierre Roux.

Gaia release for MathComp 1.17.0

This release is known to work with Coq 8.10 to 8.17 and MathComp 1.12.0 to 1.17.0. The Coq content is the same as before.

Gaia release for MathComp 1.15

This release is known to work with Coq 8.10 to 8.16 and MathComp 1.12.0 to 1.15.0. While the Coq content is the same as before.

Gaia release for MathComp 1.14.0

This release is known to work with Coq 8.10 to 8.15 and MathComp 1.12.0 to 1.14.0. While the Coq content is the same as before, the release splits Gaia into the following packages for easier reuse:

• coq-gaia-theory-of-sets: sets, cardinals, and integers following Bourbaki's Theory of Sets book
• coq-gaia-schutte: independent syntactic formalization of ordinals following Schütte and Ackermann
• coq-gaia-ordinals: implementation and properties of ordinals using set theory
• coq-gaia-numbers: implementation of algebraic structures following Bourbaki, including Z, Q, and R
• coq-gaia-stern: independent formalization of properties of Fibonacci numbers and the Stern diatomic sequence

Gaia release for MathComp 1.13.0

This is a maintenance release, known to work with Coq 8.10 to 8.14 and MathComp 1.12.0 and 1.13.0. It contains no admitted proofs.

Gaia release for MathComp 1.12.0

This is a maintenance release, known to work with Coq 8.10 to 8.14 and MathComp 1.12.0. It contains no admitted proofs.

Gaia release for MathComp 1.11.0

This is a maintenance release, known to work with Coq 8.10 to 8.12 and MathComp 1.11.0.

Gaia release for MathComp 1.9.0

This is a maintenance release, known to work with Coq 8.10.2 and MathComp 1.9.0 or 1.10.0.

Gaia release for MathComp 1.7.0

This is a maintenance release, known to work with Coq 8.9.1 and MathComp 1.7.0.