maj

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

3 files changed, 10 insertions, 10 deletions

diff --git a/.depend b/.depend
index 3763414cc..27313d9b4 100644
--- a/.depend
+++ b/.depend
@@ -2827,14 +2827,14 @@ contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     interp/constrintern.cmx toplevel/command.cmx 
 contrib/funind/indfun_common.cmo: lib/util.cmi pretyping/termops.cmi \
     kernel/term.cmi kernel/sign.cmi pretyping/rawterm.cmi lib/pp.cmi \
-    library/nametab.cmi kernel/names.cmi library/nameops.cmi \
-    library/libnames.cmi library/global.cmi kernel/declarations.cmi \
-    interp/coqlib.cmi contrib/funind/indfun_common.cmi 
+    library/nametab.cmi kernel/names.cmi library/libnames.cmi \
+    library/global.cmi kernel/declarations.cmi interp/coqlib.cmi \
+    contrib/funind/indfun_common.cmi 
 contrib/funind/indfun_common.cmx: lib/util.cmx pretyping/termops.cmx \
     kernel/term.cmx kernel/sign.cmx pretyping/rawterm.cmx lib/pp.cmx \
-    library/nametab.cmx kernel/names.cmx library/nameops.cmx \
-    library/libnames.cmx library/global.cmx kernel/declarations.cmx \
-    interp/coqlib.cmx contrib/funind/indfun_common.cmi 
+    library/nametab.cmx kernel/names.cmx library/libnames.cmx \
+    library/global.cmx kernel/declarations.cmx interp/coqlib.cmx \
+    contrib/funind/indfun_common.cmi 
 contrib/funind/indfun_main.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     interp/topconstr.cmi kernel/term.cmi tactics/tacticals.cmi \
     tactics/tacinterp.cmi proofs/tacexpr.cmo proofs/refiner.cmi \
@@ -2874,7 +2874,7 @@ contrib/funind/new_arg_principle.cmo: toplevel/vernacexpr.cmo \
     proofs/tacmach.cmi tactics/tacinterp.cmi pretyping/rawterm.cmi \
     proofs/proof_type.cmi parsing/printer.cmi parsing/ppconstr.cmi lib/pp.cmi \
     proofs/pfedit.cmi lib/options.cmi library/nametab.cmi kernel/names.cmi \
-    library/nameops.cmi library/libnames.cmi pretyping/indrec.cmi \
+    library/libnames.cmi pretyping/indrec.cmi \
     contrib/funind/indfun_common.cmi tactics/hiddentac.cmi library/global.cmi \
     interp/genarg.cmi pretyping/evd.cmi tactics/equality.cmi \
     kernel/environ.cmi kernel/entries.cmi tactics/eauto.cmi \
@@ -2889,7 +2889,7 @@ contrib/funind/new_arg_principle.cmx: toplevel/vernacexpr.cmx \
     proofs/tacmach.cmx tactics/tacinterp.cmx pretyping/rawterm.cmx \
     proofs/proof_type.cmx parsing/printer.cmx parsing/ppconstr.cmx lib/pp.cmx \
     proofs/pfedit.cmx lib/options.cmx library/nametab.cmx kernel/names.cmx \
-    library/nameops.cmx library/libnames.cmx pretyping/indrec.cmx \
+    library/libnames.cmx pretyping/indrec.cmx \
     contrib/funind/indfun_common.cmx tactics/hiddentac.cmx library/global.cmx \
     interp/genarg.cmx pretyping/evd.cmx tactics/equality.cmx \
     kernel/environ.cmx kernel/entries.cmx tactics/eauto.cmx \
diff --git a/.depend.coq b/.depend.coq
index e71783018..5ac15e7ff 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -281,7 +281,7 @@ contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/R
 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/Field.vo theories/Reals/DiscrR.vo
 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/recdef/Recdef.vo: contrib/recdef/Recdef.v theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
 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
diff --git a/make.result b/make.result
index e7e2ec5f8..8667211ca 100644
--- a/make.result
+++ b/make.result
@@ -1 +1 @@
-Thu 09/02/2006 00:30: Success
+Fri 10/02/2006 00:30: Success