math-comp / real-closed

Theorems for Real Closed Fields
13 stars 11 forks source link

compatibility with mathcomp 1.10.0 #20

Closed affeldt-aist closed 4 years ago

affeldt-aist commented 4 years ago

Compiles with mathcomp 1.10 and 1.9 (and below) at the price of some ltac in polyrcf.v to accommodate the new version of Lemma path_min_sorted.