search

math-comp / real-closed

Theorems for Real Closed Fields
13 stars 11 forks source link

Fix w.r.t. the master branches of Coq and MathComp #16

Closed pi8027 closed 4 years ago

pi8027 commented 5 years ago

This can be compiled with https://github.com/math-comp/math-comp/pull/270 without the compatibility module ssrnum.mc_1_9.

CohenCyril commented 4 years ago

Thanks! @pi8027 and @affeldt-aist!!