search

math-comp / real-closed

Theorems for Real Closed Fields
13 stars 11 forks source link

Broken on Coq bench #4

Closed SkySkimmer closed 4 years ago

SkySkimmer commented 5 years ago

https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/567/console

File "./theories/complex.v", line 1245, characters 36-57:
Error: The reference closed_fields_QEMixin was not found in the current
environment.

I guess some import changed at some point?

drouhling commented 5 years ago

This comes from a change of name in the field package (fields became field).

This should be fixed by #5