MathComp real-closed 2.0.0

Compatible with 8.16 and 8.17 and with mathcomp 2.0.0

MathComp real-closed 1.1.4

Compatible with 8.14 to 8.16 and with mathcomp 1.13.0 to 1.16.0

MathComp real-closed 1.1.3

Compatible with 8.13 to 8.15 and with mathcomp 1.12.0 to 1.15.0

MathComp real-closed 1.1.2

Compatible with 8.10 to 8.12 and with mathcomp 1.12.0

MathComp real-closed 1.1.1

The major update is the removal of the lmodType R canonical structure on complex and the introduction of Rcomplex to denote complex as an module on R without order.
Compatible with 8.7 to 8.11 and with mathcomp 1.11.0

MathComp real-closed 1.1.0

The major update is the removal of the lmodType R canonical structure on complex and the introduction of Rcomplex to denote complex as an module on R without order.
Compatible with 8.7 to 8.11 and with mathcomp 1.11.0+beta1

MathComp real-closed 1.0.5

Compatible with 8.7 to 8.11 and with mathcomp 1.11.0+beta1

MathComp Real-closed 1.0.4

A release for compatibility with MathComp 1.10.0.

coq-mathcomp-real-closed-1.0.3

This is the release of real-closed 1.0.3
Roughly in the state it was in 2012.
It compiles with Coq from 8.7 to 8.10+beta1 and mathcomp 1.8.0 and 1.9.0.

coq-mathcomp-real-closed-1.0.2

This is the release of real-closed 1.0.2
Roughly in the state it was in 2012.
It compiles with Coq >= 8.7 and mathcomp 1.8.0