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