maj

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

3 files changed, 32 insertions, 0 deletions

diff --git a/.depend b/.depend
index a7bf401dcf..e0020b2889 100644
--- a/.depend
+++ b/.depend
@@ -3452,6 +3452,30 @@ contrib/rtauto/refl_tauto.cmx: lib/util.cmx pretyping/termops.cmx \
     pretyping/retyping.cmx contrib/rtauto/proof_search.cmx lib/pp.cmx \
     kernel/names.cmx library/goptions.cmx lib/explore.cmx pretyping/evd.cmx \
     interp/coqlib.cmx kernel/closure.cmx contrib/rtauto/refl_tauto.cmi 
+contrib/setoid_ring/newring.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
+    pretyping/typing.cmi kernel/term.cmi tactics/tactics.cmi \
+    tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \
+    proofs/tacexpr.cmo library/summary.cmi tactics/setoid_replace.cmi \
+    pretyping/retyping.cmi proofs/refiner.cmi pretyping/rawterm.cmi \
+    proofs/proof_type.cmi pretyping/pretyping.cmi parsing/pptactic.cmi \
+    translate/ppconstrnew.cmi lib/pp.cmi parsing/pcoq.cmi lib/options.cmi \
+    kernel/names.cmi kernel/mod_subst.cmi library/libobject.cmi \
+    library/lib.cmi library/global.cmi interp/genarg.cmi parsing/extend.cmi \
+    pretyping/evd.cmi kernel/esubst.cmi kernel/environ.cmi \
+    parsing/egrammar.cmi interp/coqlib.cmi interp/constrintern.cmi \
+    kernel/closure.cmi toplevel/cerrors.cmi 
+contrib/setoid_ring/newring.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
+    pretyping/typing.cmx kernel/term.cmx tactics/tactics.cmx \
+    tactics/tacticals.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \
+    proofs/tacexpr.cmx library/summary.cmx tactics/setoid_replace.cmx \
+    pretyping/retyping.cmx proofs/refiner.cmx pretyping/rawterm.cmx \
+    proofs/proof_type.cmx pretyping/pretyping.cmx parsing/pptactic.cmx \
+    translate/ppconstrnew.cmx lib/pp.cmx parsing/pcoq.cmx lib/options.cmx \
+    kernel/names.cmx kernel/mod_subst.cmx library/libobject.cmx \
+    library/lib.cmx library/global.cmx interp/genarg.cmx parsing/extend.cmx \
+    pretyping/evd.cmx kernel/esubst.cmx kernel/environ.cmx \
+    parsing/egrammar.cmx interp/coqlib.cmx interp/constrintern.cmx \
+    kernel/closure.cmx toplevel/cerrors.cmx 
 contrib/subtac/eterm.cmo: pretyping/termops.cmi kernel/term.cmi \
     tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \
     contrib/subtac/sutils.cmi kernel/reduction.cmi lib/pp.cmi \
@@ -3690,6 +3714,8 @@ contrib/ring/g_ring.cmo: parsing/grammar.cma
 contrib/ring/g_ring.cmx: parsing/grammar.cma
 contrib/dp/g_dp.cmo: parsing/grammar.cma
 contrib/dp/g_dp.cmx: parsing/grammar.cma
+contrib/setoid_ring/newring.cmo: parsing/grammar.cma
+contrib/setoid_ring/newring.cmx: parsing/grammar.cma
 contrib/field/field.cmo: parsing/grammar.cma
 contrib/field/field.cmx: parsing/grammar.cma
 contrib/fourier/g_fourier.cmo: parsing/grammar.cma
diff --git a/.depend.camlp4 b/.depend.camlp4
index 63ab34d276..8ef716949d 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -9,6 +9,7 @@ contrib/romega/g_romega.ml: parsing/grammar.cma
 contrib/ring/g_quote.ml: parsing/grammar.cma
 contrib/ring/g_ring.ml: parsing/grammar.cma
 contrib/dp/g_dp.ml: parsing/grammar.cma
+contrib/setoid_ring/newring.ml: parsing/grammar.cma
 contrib/field/field.ml: parsing/grammar.cma
 contrib/fourier/g_fourier.ml: parsing/grammar.cma
 contrib/extraction/g_extraction.ml: parsing/grammar.cma
diff --git a/.depend.coq b/.depend.coq
index cc531c7b04..efc8a86c23 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -280,3 +280,8 @@ contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo con
 contrib/rtauto/Bintree.vo: contrib/rtauto/Bintree.v theories/Lists/List.vo theories/NArith/BinPos.vo
 contrib/rtauto/Rtauto.vo: contrib/rtauto/Rtauto.v theories/Lists/List.vo contrib/rtauto/Bintree.vo theories/Bool/Bool.vo theories/NArith/BinPos.vo
 contrib/recdef/Recdef.vo: contrib/recdef/Recdef.v theories/Arith/Arith.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo contrib/recdef/recdef.cmo
+contrib/setoid_ring/BinList.vo: contrib/setoid_ring/BinList.v theories/NArith/BinPos.vo
+contrib/setoid_ring/Ring_th.vo: contrib/setoid_ring/Ring_th.v theories/Setoids/Setoid.vo
+contrib/setoid_ring/Pol.vo: contrib/setoid_ring/Pol.v theories/Setoids/Setoid.vo contrib/setoid_ring/BinList.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo contrib/setoid_ring/Ring_th.vo
+contrib/setoid_ring/Ring_tac.vo: contrib/setoid_ring/Ring_tac.v theories/Setoids/Setoid.vo contrib/setoid_ring/BinList.vo theories/NArith/BinPos.vo contrib/setoid_ring/Pol.vo contrib/setoid_ring/newring.cmo
+contrib/setoid_ring/ZRing_th.vo: contrib/setoid_ring/ZRing_th.v contrib/setoid_ring/Ring_th.vo contrib/setoid_ring/Pol.vo contrib/setoid_ring/Ring_tac.vo theories/ZArith/ZArith_base.vo theories/ZArith/BinInt.vo theories/NArith/BinNat.vo theories/Setoids/Setoid.vo