maj

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

1 files changed, 22 insertions, 20 deletions

diff --git a/.depend b/.depend
index 8d634e2227..feb9c02bf9 100644
--- a/.depend
+++ b/.depend
@@ -1689,29 +1689,31 @@ toplevel/class.cmx: pretyping/classops.cmx kernel/declarations.cmx \
     pretyping/typing.cmx lib/util.cmx toplevel/class.cmi 
 toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \
     parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \
-    kernel/entries.cmi kernel/environ.cmi pretyping/evd.cmi \
-    library/global.cmi tactics/hiddentac.cmi library/impargs.cmi \
-    pretyping/indrec.cmi kernel/indtypes.cmi kernel/inductive.cmi \
-    library/lib.cmi library/libnames.cmi library/libobject.cmi \
-    library/library.cmi proofs/logic.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \
-    parsing/printer.cmi proofs/proof_type.cmi kernel/reduction.cmi \
-    proofs/refiner.cmi kernel/safe_typing.cmi library/states.cmi \
-    pretyping/syntax_def.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
-    kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi lib/util.cmi \
+    kernel/entries.cmi kernel/environ.cmi pretyping/evarutil.cmi \
+    pretyping/evd.cmi library/global.cmi tactics/hiddentac.cmi \
+    library/impargs.cmi pretyping/indrec.cmi kernel/indtypes.cmi \
+    kernel/inductive.cmi library/lib.cmi library/libnames.cmi \
+    library/libobject.cmi library/library.cmi proofs/logic.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \
+    kernel/reduction.cmi proofs/refiner.cmi pretyping/retyping.cmi \
+    kernel/safe_typing.cmi library/states.cmi pretyping/syntax_def.cmi \
+    proofs/tacmach.cmi pretyping/tacred.cmi kernel/term.cmi \
+    pretyping/termops.cmi kernel/typeops.cmi lib/util.cmi \
     toplevel/vernacexpr.cmo toplevel/command.cmi 
 toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \
     parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \
-    kernel/entries.cmx kernel/environ.cmx pretyping/evd.cmx \
-    library/global.cmx tactics/hiddentac.cmx library/impargs.cmx \
-    pretyping/indrec.cmx kernel/indtypes.cmx kernel/inductive.cmx \
-    library/lib.cmx library/libnames.cmx library/libobject.cmx \
-    library/library.cmx proofs/logic.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \
-    parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \
-    proofs/refiner.cmx kernel/safe_typing.cmx library/states.cmx \
-    pretyping/syntax_def.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
-    kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx lib/util.cmx \
+    kernel/entries.cmx kernel/environ.cmx pretyping/evarutil.cmx \
+    pretyping/evd.cmx library/global.cmx tactics/hiddentac.cmx \
+    library/impargs.cmx pretyping/indrec.cmx kernel/indtypes.cmx \
+    kernel/inductive.cmx library/lib.cmx library/libnames.cmx \
+    library/libobject.cmx library/library.cmx proofs/logic.cmx \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \
+    kernel/reduction.cmx proofs/refiner.cmx pretyping/retyping.cmx \
+    kernel/safe_typing.cmx library/states.cmx pretyping/syntax_def.cmx \
+    proofs/tacmach.cmx pretyping/tacred.cmx kernel/term.cmx \
+    pretyping/termops.cmx kernel/typeops.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx toplevel/command.cmi 
 toplevel/coqinit.cmo: config/coq_config.cmi toplevel/mltop.cmi \
     library/nameops.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \