Compilation newring

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

5 files changed, 72 insertions, 58 deletions

diff --git a/.depend b/.depend
index 068350d28..1e730c2d0 100644
--- a/.depend
+++ b/.depend
@@ -1337,15 +1337,17 @@ pretyping/classops.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
     pretyping/rawterm.cmi lib/pp.cmi lib/options.cmi library/nametab.cmi \
     kernel/names.cmi kernel/mod_subst.cmi library/library.cmi \
     library/libobject.cmi library/libnames.cmi library/lib.cmi \
-    library/goptions.cmi lib/gmap.cmi library/global.cmi pretyping/evd.cmi \
-    kernel/environ.cmi library/decl_kinds.cmo pretyping/classops.cmi 
+    pretyping/inductiveops.cmi library/goptions.cmi lib/gmap.cmi \
+    library/global.cmi pretyping/evd.cmi kernel/environ.cmi \
+    library/decl_kinds.cmo pretyping/classops.cmi 
 pretyping/classops.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \
     pretyping/tacred.cmx library/summary.cmx pretyping/reductionops.cmx \
     pretyping/rawterm.cmx lib/pp.cmx lib/options.cmx library/nametab.cmx \
     kernel/names.cmx kernel/mod_subst.cmx library/library.cmx \
     library/libobject.cmx library/libnames.cmx library/lib.cmx \
-    library/goptions.cmx lib/gmap.cmx library/global.cmx pretyping/evd.cmx \
-    kernel/environ.cmx library/decl_kinds.cmx pretyping/classops.cmi 
+    pretyping/inductiveops.cmx library/goptions.cmx lib/gmap.cmx \
+    library/global.cmx pretyping/evd.cmx kernel/environ.cmx \
+    library/decl_kinds.cmx pretyping/classops.cmi 
 pretyping/clenv.cmo: lib/util.cmi pretyping/unification.cmi \
     pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \
     pretyping/tacred.cmi proofs/tacexpr.cmo kernel/sign.cmi \
@@ -4107,66 +4109,74 @@ tools/coq_makefile.cmx:
 tools/coq-tex.cmo: 
 tools/coq-tex.cmx: 
 coq_fix_code.o: kernel/byterun/coq_fix_code.c \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/misc.h /usr/lib/ocaml/caml/config.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/mlvalues.h \
-  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/config.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/fail.h /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_instruct.h \
   kernel/byterun/coq_fix_code.h
 coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \
-  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
-  kernel/byterun/coq_jumptbl.h
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/alloc.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+  /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \
+  kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
 coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \
-  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/memory.h
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/alloc.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+  /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h
 coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/fail.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
-  /usr/lib/ocaml/caml/alloc.h
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_values.h \
+  /usr/lib/ocaml/3.09.2/caml/alloc.h
 coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/misc.h /usr/lib/ocaml/caml/config.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/mlvalues.h \
-  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/config.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/fail.h /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_instruct.h \
   kernel/byterun/coq_fix_code.h
 coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \
-  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
-  kernel/byterun/coq_jumptbl.h
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/alloc.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+  /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \
+  kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
 coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \
-  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/memory.h
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/alloc.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+  /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h
 coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/fail.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
-  /usr/lib/ocaml/caml/alloc.h
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_values.h \
+  /usr/lib/ocaml/3.09.2/caml/alloc.h
diff --git a/.depend.coq b/.depend.coq
index 59ad870a6..f15ba9f2d 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -340,7 +340,7 @@ contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/romega/ReflOmegaCore.v
 contrib/ring/LegacyArithRing.vo: contrib/ring/LegacyArithRing.v theories/Bool/Bool.vo contrib/ring/LegacyRing.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
 contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/LegacyRing_theory.vo contrib/ring/Quote.vo
 contrib/ring/LegacyRing_theory.vo: contrib/ring/LegacyRing_theory.v theories/Bool/Bool.vo
-contrib/ring/LegacyRing.vo: contrib/ring/LegacyRing.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo
+contrib/ring/LegacyRing.vo: contrib/ring/LegacyRing.v theories/Bool/Bool.vo contrib/ring/LegacyRing_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo
 contrib/ring/LegacyNArithRing.vo: contrib/ring/LegacyNArithRing.v theories/Bool/Bool.vo contrib/ring/LegacyRing.vo theories/ZArith/ZArith_base.vo theories/NArith/NArith.vo theories/Logic/Eqdep_dec.vo
 contrib/ring/LegacyZArithRing.vo: contrib/ring/LegacyZArithRing.v contrib/setoid_ring/ArithRing.vo theories/ZArith/ZArith_base.vo theories/Logic/Eqdep_dec.vo
 contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/LegacyRing_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo
@@ -365,6 +365,7 @@ contrib/setoid_ring/Ring_equiv.vo: contrib/setoid_ring/Ring_equiv.v contrib/ring
 contrib/setoid_ring/Ring_base.vo: contrib/setoid_ring/Ring_base.v contrib/setoid_ring/newring.cmo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_tac.vo
 contrib/setoid_ring/Ring.vo: contrib/setoid_ring/Ring.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Ring_equiv.vo
 contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith/Arith.vo contrib/setoid_ring/Ring.vo
+contrib/setoid_ring/Ring_polynom.vo: contrib/setoid_ring/Ring_polynom.v theories/Setoids/Setoid.vo contrib/setoid_ring/BinList.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo contrib/setoid_ring/Ring_theory.vo
 contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v theories/NArith/NArith.vo contrib/setoid_ring/Ring.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.vo: contrib/setoid_ring/Field.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo
diff --git a/Makefile b/Makefile
index 40a46316a..85c8efde0 100644
--- a/Makefile
+++ b/Makefile
@@ -1047,7 +1047,7 @@ NEWRINGVO=\
  contrib/setoid_ring/Pol.vo       contrib/setoid_ring/Ring_tac.vo \
  contrib/setoid_ring/ZRing_th.vo  contrib/setoid_ring/Ring_equiv.vo \
  contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/Ring.vo \
- contrib/setoid_ring/ArithRing.vo \
+ contrib/setoid_ring/ArithRing.vo contrib/setoid_ring/Ring_polynom.vo \
  contrib/setoid_ring/NArithRing.vo \
  contrib/setoid_ring/ZArithRing.vo \
 contrib/setoid_ring/Field.vo \
diff --git a/contrib/ring/LegacyZArithRing.v b/contrib/ring/LegacyZArithRing.v
index 075431827..9669d4f86 100644
--- a/contrib/ring/LegacyZArithRing.v
+++ b/contrib/ring/LegacyZArithRing.v
@@ -13,6 +13,7 @@
 Require Export ArithRing.
 Require Export ZArith_base.
 Require Import Eqdep_dec.
+Require Import LegacyRing.
 
 Unboxed Definition Zeq (x y:Z) :=
   match (x ?= y)%Z with
diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v
index e322d9e21..abee90b13 100644
--- a/contrib/setoid_ring/NArithRing.v
+++ b/contrib/setoid_ring/NArithRing.v
@@ -8,6 +8,8 @@
 
 Require Import NArith.
 Require Export Ring.
+Require Import InitialRing.
+
 Set Implicit Arguments.
 
 Ltac isNcst t :=