ler_to_alg does not compile

[jaapb]

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]

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.