ler_to_alg does not compile

math-comp / real-closed

Theorems for Real Closed Fields

13 stars 11 forks source link

ler_to_alg does not compile #6

Closed jaapb closed 4 years ago

jaapb commented 5 years ago

When compiling with coq 8.8 and 8.9 (beta, I didn't check 8.9.0 yet), theories/realalg.v fails to compile with the following message (at line 976 in ler_to_alg):

Ltac call to "apply (ssrapplyarg)" failed. Ltac call to "apply (ssrapplyarg)" failed. No assumption in (?s (to_alg_def (Phant F) x) = x)

amahboubi commented 5 years ago

Hello @jaapb. This is a very late answer, but in case you're still interested, there is an existing PR which makes real-closed work with math-comp 1.8 (at least). It is about to be released:see #17.