Releases: math-comp/real-closed
MathComp real-closed 2.0.1
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.