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

7 files changed, 62 insertions, 50 deletions

diff --git a/.depend b/.depend
index 18778724dc..25db9cebe1 100644
--- a/.depend
+++ b/.depend
@@ -292,7 +292,7 @@ tactics/equality.cmi: kernel/term.cmi tactics/tactics.cmi \
     tactics/tacticals.cmi proofs/tacmach.cmi proofs/tacexpr.cmo \
     kernel/sign.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \
     pretyping/pattern.cmi kernel/names.cmi tactics/hipattern.cmi \
-    pretyping/evd.cmi kernel/environ.cmi 
+    interp/genarg.cmi pretyping/evd.cmi kernel/environ.cmi 
 tactics/evar_tactics.cmi: kernel/term.cmi proofs/tacmach.cmi \
     proofs/tacexpr.cmo pretyping/rawterm.cmi kernel/names.cmi 
 tactics/extraargs.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \
@@ -590,8 +590,8 @@ ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \
     config/coq_config.cmx toplevel/cerrors.cmx ide/coq.cmi 
 ide/coq_tactics.cmo: ide/coq_tactics.cmi 
 ide/coq_tactics.cmx: ide/coq_tactics.cmi 
-ide/find_phrase.cmo: ide/ideutils.cmi 
-ide/find_phrase.cmx: ide/ideutils.cmx 
+ide/find_phrase.cmo: ide/preferences.cmi ide/ideutils.cmi 
+ide/find_phrase.cmx: ide/preferences.cmx ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmi 
 ide/highlight.cmx: ide/ideutils.cmx 
 ide/ideutils.cmo: ide/utf8_convert.cmo lib/system.cmi ide/preferences.cmi \
@@ -695,13 +695,13 @@ interp/syntax_def.cmx: lib/util.cmx interp/topconstr.cmx library/summary.cmx \
     kernel/names.cmx library/nameops.cmx library/libobject.cmx \
     library/libnames.cmx library/lib.cmx interp/syntax_def.cmi 
 interp/topconstr.cmo: lib/util.cmi kernel/term.cmi pretyping/rawterm.cmi \
-    lib/pp.cmi kernel/names.cmi library/nameops.cmi kernel/mod_subst.cmi \
-    library/libnames.cmi pretyping/evd.cmi lib/dyn.cmi pretyping/detyping.cmi \
-    lib/bigint.cmi interp/topconstr.cmi 
+    lib/pp.cmi library/nametab.cmi kernel/names.cmi library/nameops.cmi \
+    kernel/mod_subst.cmi library/libnames.cmi pretyping/evd.cmi lib/dyn.cmi \
+    pretyping/detyping.cmi lib/bigint.cmi interp/topconstr.cmi 
 interp/topconstr.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \
-    lib/pp.cmx kernel/names.cmx library/nameops.cmx kernel/mod_subst.cmx \
-    library/libnames.cmx pretyping/evd.cmx lib/dyn.cmx pretyping/detyping.cmx \
-    lib/bigint.cmx interp/topconstr.cmi 
+    lib/pp.cmx library/nametab.cmx kernel/names.cmx library/nameops.cmx \
+    kernel/mod_subst.cmx library/libnames.cmx pretyping/evd.cmx lib/dyn.cmx \
+    pretyping/detyping.cmx lib/bigint.cmx interp/topconstr.cmi 
 kernel/cbytecodes.cmo: kernel/term.cmi kernel/names.cmi kernel/cbytecodes.cmi 
 kernel/cbytecodes.cmx: kernel/term.cmx kernel/names.cmx kernel/cbytecodes.cmi 
 kernel/cbytegen.cmo: lib/util.cmi kernel/term.cmi kernel/pre_env.cmi \
@@ -764,10 +764,12 @@ kernel/indtypes.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \
     kernel/entries.cmx kernel/declarations.cmx kernel/indtypes.cmi 
 kernel/inductive.cmo: lib/util.cmi kernel/univ.cmi kernel/type_errors.cmi \
     kernel/term.cmi kernel/sign.cmi kernel/reduction.cmi kernel/names.cmi \
-    kernel/environ.cmi kernel/declarations.cmi kernel/inductive.cmi 
+    kernel/environ.cmi kernel/declarations.cmi kernel/closure.cmi \
+    kernel/inductive.cmi 
 kernel/inductive.cmx: lib/util.cmx kernel/univ.cmx kernel/type_errors.cmx \
     kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx kernel/names.cmx \
-    kernel/environ.cmx kernel/declarations.cmx kernel/inductive.cmi 
+    kernel/environ.cmx kernel/declarations.cmx kernel/closure.cmx \
+    kernel/inductive.cmi 
 kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \
     kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \
     kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \
@@ -1317,7 +1319,7 @@ pretyping/cases.cmo: lib/util.cmi kernel/typeops.cmi kernel/type_errors.cmi \
     library/nameops.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \
     library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
     pretyping/evarconv.cmi kernel/environ.cmi kernel/declarations.cmi \
-    pretyping/coercion.cmi pretyping/cases.cmi 
+    pretyping/coercion.cmi kernel/closure.cmi pretyping/cases.cmi 
 pretyping/cases.cmx: lib/util.cmx kernel/typeops.cmx kernel/type_errors.cmx \
     pretyping/termops.cmx kernel/term.cmx kernel/sign.cmx \
     pretyping/retyping.cmx pretyping/reductionops.cmx pretyping/rawterm.cmx \
@@ -1325,7 +1327,7 @@ pretyping/cases.cmx: lib/util.cmx kernel/typeops.cmx kernel/type_errors.cmx \
     library/nameops.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \
     library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
     pretyping/evarconv.cmx kernel/environ.cmx kernel/declarations.cmx \
-    pretyping/coercion.cmx pretyping/cases.cmi 
+    pretyping/coercion.cmx kernel/closure.cmx pretyping/cases.cmi 
 pretyping/cbv.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \
     kernel/names.cmi pretyping/evd.cmi kernel/esubst.cmi kernel/environ.cmi \
     kernel/conv_oracle.cmi kernel/closure.cmi pretyping/cbv.cmi 
@@ -1366,18 +1368,18 @@ pretyping/clenv.cmx: lib/util.cmx pretyping/unification.cmx \
     kernel/mod_subst.cmx library/global.cmx pretyping/evd.cmx \
     pretyping/evarutil.cmx kernel/environ.cmx pretyping/coercion.cmx \
     pretyping/clenv.cmi 
-pretyping/coercion.cmo: lib/util.cmi kernel/typeops.cmi kernel/term.cmi \
-    pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \
-    pretyping/recordops.cmi pretyping/rawterm.cmi \
-    pretyping/pretype_errors.cmi lib/pp.cmi kernel/names.cmi \
-    pretyping/evd.cmi pretyping/evarutil.cmi pretyping/evarconv.cmi \
-    kernel/environ.cmi pretyping/classops.cmi pretyping/coercion.cmi 
-pretyping/coercion.cmx: lib/util.cmx kernel/typeops.cmx kernel/term.cmx \
-    pretyping/retyping.cmx pretyping/reductionops.cmx kernel/reduction.cmx \
-    pretyping/recordops.cmx pretyping/rawterm.cmx \
-    pretyping/pretype_errors.cmx lib/pp.cmx kernel/names.cmx \
-    pretyping/evd.cmx pretyping/evarutil.cmx pretyping/evarconv.cmx \
-    kernel/environ.cmx pretyping/classops.cmx pretyping/coercion.cmi 
+pretyping/coercion.cmo: lib/util.cmi kernel/typeops.cmi pretyping/termops.cmi \
+    kernel/term.cmi pretyping/retyping.cmi pretyping/reductionops.cmi \
+    kernel/reduction.cmi pretyping/recordops.cmi pretyping/rawterm.cmi \
+    pretyping/pretype_errors.cmi kernel/names.cmi pretyping/evd.cmi \
+    pretyping/evarutil.cmi pretyping/evarconv.cmi kernel/environ.cmi \
+    pretyping/classops.cmi pretyping/coercion.cmi 
+pretyping/coercion.cmx: lib/util.cmx kernel/typeops.cmx pretyping/termops.cmx \
+    kernel/term.cmx pretyping/retyping.cmx pretyping/reductionops.cmx \
+    kernel/reduction.cmx pretyping/recordops.cmx pretyping/rawterm.cmx \
+    pretyping/pretype_errors.cmx kernel/names.cmx pretyping/evd.cmx \
+    pretyping/evarutil.cmx pretyping/evarconv.cmx kernel/environ.cmx \
+    pretyping/classops.cmx pretyping/coercion.cmi 
 pretyping/detyping.cmo: lib/util.cmi kernel/univ.cmi pretyping/termops.cmi \
     kernel/term.cmi kernel/sign.cmi pretyping/rawterm.cmi lib/pp.cmi \
     lib/options.cmi library/nametab.cmi kernel/names.cmi library/nameops.cmi \
@@ -1785,13 +1787,15 @@ tactics/btermdn.cmo: tactics/termdn.cmi kernel/term.cmi pretyping/pattern.cmi \
 tactics/btermdn.cmx: tactics/termdn.cmx kernel/term.cmx pretyping/pattern.cmx \
     library/libnames.cmx tactics/dn.cmx tactics/btermdn.cmi 
 tactics/contradiction.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \
-    tactics/tacticals.cmi proofs/tacmach.cmi pretyping/reductionops.cmi \
-    pretyping/rawterm.cmi proofs/proof_type.cmi tactics/hipattern.cmi \
-    interp/coqlib.cmi tactics/contradiction.cmi 
+    tactics/tacticals.cmi proofs/tacmach.cmi pretyping/retyping.cmi \
+    pretyping/reductionops.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \
+    tactics/hipattern.cmi pretyping/evd.cmi kernel/environ.cmi \
+    interp/coqlib.cmi pretyping/coercion.cmi tactics/contradiction.cmi 
 tactics/contradiction.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \
-    tactics/tacticals.cmx proofs/tacmach.cmx pretyping/reductionops.cmx \
-    pretyping/rawterm.cmx proofs/proof_type.cmx tactics/hipattern.cmx \
-    interp/coqlib.cmx tactics/contradiction.cmi 
+    tactics/tacticals.cmx proofs/tacmach.cmx pretyping/retyping.cmx \
+    pretyping/reductionops.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \
+    tactics/hipattern.cmx pretyping/evd.cmx kernel/environ.cmx \
+    interp/coqlib.cmx pretyping/coercion.cmx tactics/contradiction.cmi 
 tactics/decl_interp.cmo: lib/util.cmi interp/topconstr.cmi \
     pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi \
     tactics/tacinterp.cmi pretyping/rawterm.cmi pretyping/pretyping.cmi \
@@ -3104,6 +3108,14 @@ contrib/funind/invfun.cmx: toplevel/vernacentries.cmx lib/util.cmx \
     kernel/entries.cmx kernel/declarations.cmx library/decl_kinds.cmx \
     interp/coqlib.cmx toplevel/command.cmx kernel/closure.cmx \
     toplevel/cerrors.cmx 
+contrib/funind/merge.cmo: lib/util.cmi kernel/term.cmi \
+    contrib/funind/tacinvutils.cmi tactics/tacinterp.cmi kernel/names.cmi \
+    pretyping/inductiveops.cmi kernel/inductive.cmi library/global.cmi \
+    pretyping/evd.cmi kernel/environ.cmi kernel/declarations.cmi 
+contrib/funind/merge.cmx: lib/util.cmx kernel/term.cmx \
+    contrib/funind/tacinvutils.cmx tactics/tacinterp.cmx kernel/names.cmx \
+    pretyping/inductiveops.cmx kernel/inductive.cmx library/global.cmx \
+    pretyping/evd.cmx kernel/environ.cmx kernel/declarations.cmx 
 contrib/funind/rawtermops.cmo: lib/util.cmi pretyping/rawterm.cmi lib/pp.cmi \
     kernel/names.cmi library/nameops.cmi library/libnames.cmi \
     pretyping/inductiveops.cmi contrib/funind/indfun_common.cmi \
@@ -3780,14 +3792,14 @@ contrib/subtac/subtac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     toplevel/cerrors.cmx contrib/subtac/subtac.cmi 
 contrib/subtac/subtac_obligations.cmo: lib/util.cmi kernel/term.cmi \
     library/summary.cmi contrib/subtac/subtac_utils.cmi lib/pp.cmi \
-    kernel/names.cmi library/libobject.cmi library/libnames.cmi \
-    kernel/entries.cmi library/declare.cmi library/decl_kinds.cmo \
-    toplevel/command.cmi 
+    lib/options.cmi kernel/names.cmi library/libobject.cmi \
+    library/libnames.cmi kernel/entries.cmi library/declare.cmi \
+    library/decl_kinds.cmo toplevel/command.cmi 
 contrib/subtac/subtac_obligations.cmx: lib/util.cmx kernel/term.cmx \
     library/summary.cmx contrib/subtac/subtac_utils.cmx lib/pp.cmx \
-    kernel/names.cmx library/libobject.cmx library/libnames.cmx \
-    kernel/entries.cmx library/declare.cmx library/decl_kinds.cmx \
-    toplevel/command.cmx 
+    lib/options.cmx kernel/names.cmx library/libobject.cmx \
+    library/libnames.cmx kernel/entries.cmx library/declare.cmx \
+    library/decl_kinds.cmx toplevel/command.cmx 
 contrib/subtac/subtac_pretyping_F.cmo: lib/util.cmi kernel/typeops.cmi \
     kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \
     kernel/sign.cmi pretyping/retyping.cmi pretyping/reductionops.cmi \
diff --git a/.depend.coq b/.depend.coq
index e4ec4b5ce3..3fe8e475c2 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -348,10 +348,10 @@ contrib/ring/Quote.vo: contrib/ring/Quote.v
 contrib/ring/Setoid_ring_normalize.vo: contrib/ring/Setoid_ring_normalize.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo
 contrib/ring/Setoid_ring.vo: contrib/ring/Setoid_ring.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo
 contrib/ring/Setoid_ring_theory.vo: contrib/ring/Setoid_ring_theory.v theories/Bool/Bool.vo theories/Setoids/Setoid.vo
-contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v theories/Lists/List.vo
-contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Lists/List.vo theories/Arith/Peano_dec.vo contrib/ring/LegacyRing.vo contrib/field/Field_Compl.vo
-contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v theories/Lists/List.vo contrib/ring/LegacyRing.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo
-contrib/field/LegacyField.vo: contrib/field/LegacyField.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo
+contrib/field/LegacyField_Compl.vo: contrib/field/LegacyField_Compl.v theories/Lists/List.vo
+contrib/field/LegacyField_Theory.vo: contrib/field/LegacyField_Theory.v theories/Lists/List.vo theories/Arith/Peano_dec.vo contrib/ring/LegacyRing.vo contrib/field/LegacyField_Compl.vo
+contrib/field/LegacyField_Tactic.vo: contrib/field/LegacyField_Tactic.v theories/Lists/List.vo contrib/ring/LegacyRing.vo contrib/field/LegacyField_Compl.vo contrib/field/LegacyField_Theory.vo
+contrib/field/LegacyField.vo: contrib/field/LegacyField.v contrib/field/LegacyField_Compl.vo contrib/field/LegacyField_Theory.vo contrib/field/LegacyField_Tactic.vo
 contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo
 contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/LegacyField.vo theories/Reals/DiscrR.vo
 contrib/subtac/FixSub.vo: contrib/subtac/FixSub.v theories/Init/Wf.vo theories/Arith/Wf_nat.vo theories/Arith/Lt.vo
@@ -371,6 +371,6 @@ contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith
 contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo
 contrib/setoid_ring/ZArithRing.vo: contrib/setoid_ring/ZArithRing.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo
 contrib/setoid_ring/Field_theory.vo: contrib/setoid_ring/Field_theory.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo
-contrib/setoid_ring/Field_tac.vo: contrib/setoid_ring/Field_tac.v contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field_theory.vo
+contrib/setoid_ring/Field_tac.vo: contrib/setoid_ring/Field_tac.v contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/BinList.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field_theory.vo
 contrib/setoid_ring/Field.vo: contrib/setoid_ring/Field.v contrib/setoid_ring/Field_theory.vo contrib/setoid_ring/Field_tac.vo
 contrib/setoid_ring/RealField.vo: contrib/setoid_ring/RealField.v theories/Reals/Raxioms.vo theories/Reals/Rdefinitions.vo contrib/setoid_ring/Ring.vo contrib/setoid_ring/Field.vo
diff --git a/Makefile b/Makefile
index c03681aeee..831f703337 100644
--- a/Makefile
+++ b/Makefile
@@ -1048,8 +1048,8 @@ RINGVO=\
  contrib/ring/Setoid_ring.vo		contrib/ring/Setoid_ring_theory.vo
 
 FIELDVO=\
- contrib/field/Field_Compl.vo     contrib/field/Field_Theory.vo \
- contrib/field/Field_Tactic.vo    contrib/field/LegacyField.vo
+ contrib/field/LegacyField_Compl.vo     contrib/field/LegacyField_Theory.vo \
+ contrib/field/LegacyField_Tactic.vo    contrib/field/LegacyField.vo
 
 NEWRINGVO=\
  contrib/setoid_ring/BinList.vo   	contrib/setoid_ring/Ring_theory.vo \
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 ();