From 8fe195799d9bf4eb0c84fad3e9a79b78e6e224ec Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 16 Oct 2006 16:17:31 +0000
Subject: typo doc + bug legacy field

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9243 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/field/field.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib')

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))
-- 
cgit v1.2.3