maj

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

3 files changed, 18 insertions, 22 deletions

diff --git a/.depend b/.depend
index 12cef1b9bc..4af557c6a9 100644
--- a/.depend
+++ b/.depend
@@ -3112,10 +3112,12 @@ contrib/ring/ring.cmx: kernel/closure.cmx interp/constrintern.cmx \
     tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
     pretyping/typing.cmx lib/util.cmx toplevel/vernacexpr.cmx \
     toplevel/vernacinterp.cmx 
-contrib/romega/const_omega.cmo: interp/coqlib.cmi library/libnames.cmi \
-    kernel/names.cmi library/nametab.cmi kernel/term.cmi lib/util.cmi 
-contrib/romega/const_omega.cmx: interp/coqlib.cmx library/libnames.cmx \
-    kernel/names.cmx library/nametab.cmx kernel/term.cmx lib/util.cmx 
+contrib/romega/const_omega.cmo: interp/coqlib.cmi library/global.cmi \
+    library/libnames.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    kernel/term.cmi lib/util.cmi 
+contrib/romega/const_omega.cmx: interp/coqlib.cmx library/global.cmx \
+    library/libnames.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    kernel/term.cmx lib/util.cmx 
 contrib/romega/g_romega.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
     lib/options.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
     proofs/refiner.cmi contrib/romega/refl_omega.cmo proofs/tacexpr.cmo \
@@ -3124,22 +3126,16 @@ contrib/romega/g_romega.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     lib/options.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
     proofs/refiner.cmx contrib/romega/refl_omega.cmx proofs/tacexpr.cmx \
     tactics/tacinterp.cmx 
-contrib/romega/refl_omega.cmo: parsing/ast.cmi tactics/auto.cmi \
-    proofs/clenv.cmi contrib/romega/const_omega.cmo \
-    contrib/omega/coq_omega.cmo kernel/environ.cmi kernel/inductive.cmi \
-    library/library.cmi proofs/logic.cmi kernel/names.cmi \
-    contrib/omega/omega.cmo lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
-    kernel/term.cmi lib/util.cmi 
-contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
-    proofs/clenv.cmx contrib/romega/const_omega.cmx \
-    contrib/omega/coq_omega.cmx kernel/environ.cmx kernel/inductive.cmx \
-    library/library.cmx proofs/logic.cmx kernel/names.cmx \
-    contrib/omega/omega.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
-    kernel/term.cmx lib/util.cmx 
+contrib/romega/omega2.cmo: kernel/names.cmi lib/util.cmi 
+contrib/romega/omega2.cmx: kernel/names.cmx lib/util.cmx 
+contrib/romega/refl_omega.cmo: contrib/romega/const_omega.cmo \
+    proofs/logic.cmi kernel/names.cmi contrib/romega/omega2.cmo lib/pp.cmi \
+    parsing/printer.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi lib/util.cmi 
+contrib/romega/refl_omega.cmx: contrib/romega/const_omega.cmx \
+    proofs/logic.cmx kernel/names.cmx contrib/romega/omega2.cmx lib/pp.cmx \
+    parsing/printer.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
 contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi 
 contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx 
 contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \
diff --git a/.depend.coq b/.depend.coq
index b78c2ce22e..95233f2e5d 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -256,7 +256,7 @@ theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relatio
 theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
 contrib/omega/OmegaLemmas.vo: contrib/omega/OmegaLemmas.v theories/ZArith/ZArith_base.vo
 contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/ZArith/Zhints.vo
-contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/List.vo theories/Bool/Bool.vo theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo
+contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/List.vo theories/Bool/Bool.vo theories/ZArith/ZArith.vo contrib/omega/OmegaLemmas.vo theories/Logic/Decidable.vo
 contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/omega/Omega.vo contrib/romega/ReflOmegaCore.vo
 contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
 contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
diff --git a/make.result b/make.result
index 1fd9e87a7e..4b4bec526b 100644
--- a/make.result
+++ b/make.result
@@ -1 +1 @@
-Wed 03/03/2004 01:00: Success
+Thu 04/03/2004 01:00: Failure