4 files changed, 6 insertions, 6 deletions
diff --git a/contrib/field/LegacyField.v b/contrib/field/LegacyField.v
index 5d08c57f46..ee1ddd477b 100644
--- a/contrib/field/LegacyField.v
+++ b/contrib/field/LegacyField.v
@@ -8,8 +8,8 @@
 
 (* $Id$ *)
 
-Require Export Field_Compl.
-Require Export Field_Theory.
-Require Export Field_Tactic.
+Require Export LegacyField_Compl.
+Require Export LegacyField_Theory.
+Require Export LegacyField_Tactic.
 
-(* Command declarations are moved to the ML side *)
-\ No newline at end of file
+(* Command declarations are moved to the ML side *)
diff --git a/contrib/field/Field_Compl.v b/contrib/field/LegacyField_Compl.v
index 746e7c9976..746e7c9976 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/LegacyField_Compl.v
diff --git a/contrib/field/Field_Theory.v b/contrib/field/LegacyField_Theory.v
index a54c54a0bd..5516f92fac 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/LegacyField_Theory.v
@@ -11,7 +11,7 @@
 Require Import List.
 Require Import Peano_dec.
 Require Import LegacyRing.
-Require Import Field_Compl.
+Require Import LegacyField_Compl.
 
 Record Field_Theory : Type := 
   {A : Type;
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 2da5e9fbd7..b8a978d84e 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -86,7 +86,7 @@ let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
       Ring.add_theory true true false a None None None aplus amult aone azero
         (Some aopp) aeq rth Quote.ConstrSet.empty
      with | UserError("Add Semi Ring",_) -> ());
-    let th = mkApp ((constant ["Field_Theory"] "Build_Field_Theory"),
+    let th = mkApp ((constant ["LegacyField_Theory"] "Build_Field_Theory"),
       [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in
     begin
       let _ = type_of (Global.env ()) Evd.empty th in ();