From 5cafd34c36a63a60f22ab10ed3a251250b4635c3 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 4 Mar 2004 00:04:04 +0000 Subject: maj git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5429 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 36 ++++++++++++++++-------------------- .depend.coq | 2 +- make.result | 2 +- 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 -- cgit v1.2.3