MathComp Analysis 0.3.7

Compatible with MathComp 1.12.0, Coq 8.11, 8.12, and 8.13, and hierarchy-builder 1.1.0

See the changelog

MathComp Analysis 0.3.6

Compatible with MathComp 1.12.0, and Coq 8.11, 8.12, and 8.13.

See the changelog

MathComp Analysis 0.3.5

Compatible with MathComp 1.12.0, and Coq 8.11 and 8.12.

See the changelog

MathComp Analysis 0.3.4

Compatible with MathComp 1.11 and Coq 8.11 and 8.12

The main changes are improvements to measure theory (that now requires coq-hierarchy-builder), lemmas
about intervals, etc.

See the changelog.

MathComp Analysis 0.3.3

Compatible with MathComp 1.11.0 and Coq >= 8.10.

The main changes are improvements to the theories of classical sets and of extended reals.

See the changelog.

MathComp Analysis 0.3.2

Compatible with MathComp 1.11.0 and Coq >= 8.10.

The main changes are the insertion of a structure of uniform space to the mathcomp-analysis hierarchy and several improvements to the theories of sequences and of extended real numbers to prove Boole's inequality.

See the changelog

MathComp Analysis 0.3.1

Compatible with MathComp 1.11.0 and coq >= 8.10.

The main addition is the ordered structure iso between [-1, 1] and extended reals ([-oo, +oo]), and the proof of equivalence between the topology induced by the latter iso on extended reals as a pseudo-metric type, and the topology generated by the canonical open basis (i.e. the ]a, b[, ]a, +oo], [-oo, b]).

See the changelog

MathComp Analysis 0.3.0

Compatible with MathComp 1.11+beta1.

The biggest change of this release is compatibility with MathComp 1.11+beta1. The latter introduces in particular ordered types.
All norms and absolute values have been unified, both in their denotation `|_| and in their theory.

changelog

MathComp Analysis 0.2.3

Compatible with mathcomp 1.8.0, 1.9.0, and 1.10.0.

Mathcomp Analysis 0.2.2

Compatible with both mathcomp 1.8.0 and 1.9.0