conflit de nom (Field_theory) modulo la casse

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9273 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 6 insertions, 6 deletions

diff --git a/contrib/field/LegacyField.v b/contrib/field/LegacyField.v
index 5d08c57f4..ee1ddd477 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 746e7c997..746e7c997 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 a54c54a0b..5516f92fa 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 2da5e9fbd..b8a978d84 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 ();