aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/field/field.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index f8f872134e..2da5e9fbd7 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -175,7 +175,7 @@ let guess_theory env evc = function
(* Guesses the type and calls Field_Term with the right theory *)
let field_term l g =
- Coqlib.check_required_library ["Coq";"field";"Field"];
+ Coqlib.check_required_library ["Coq";"field";"LegacyField"];
let env = (pf_env g)
and evc = (project g) in
let th = valueIn (VConstr (guess_theory env evc l))