maj

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

1 files changed, 28 insertions, 26 deletions

diff --git a/.depend b/.depend
index ceef86450..9732c6cba 100644
--- a/.depend
+++ b/.depend
@@ -1739,10 +1739,10 @@ tactics/auto.cmo: toplevel/vernacexpr.cmo lib/util.cmi pretyping/typing.cmi \
     kernel/mod_subst.cmi pretyping/matching.cmi proofs/logic.cmi \
     library/library.cmi library/libobject.cmi library/libnames.cmi \
     library/lib.cmi kernel/inductive.cmi tactics/hipattern.cmi \
-    tactics/hiddentac.cmi library/global.cmi pretyping/evd.cmi \
-    proofs/evar_refiner.cmi kernel/environ.cmi tactics/dhyp.cmi \
-    kernel/declarations.cmi interp/constrintern.cmi pretyping/clenv.cmi \
-    tactics/btermdn.cmi tactics/auto.cmi 
+    tactics/hiddentac.cmi library/global.cmi interp/genarg.cmi \
+    pretyping/evd.cmi proofs/evar_refiner.cmi kernel/environ.cmi \
+    tactics/dhyp.cmi kernel/declarations.cmi interp/constrintern.cmi \
+    pretyping/clenv.cmi tactics/btermdn.cmi tactics/auto.cmi 
 tactics/auto.cmx: toplevel/vernacexpr.cmx lib/util.cmx pretyping/typing.cmx \
     pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \
     tactics/tacticals.cmx pretyping/tacred.cmx proofs/tacmach.cmx \
@@ -1754,10 +1754,10 @@ tactics/auto.cmx: toplevel/vernacexpr.cmx lib/util.cmx pretyping/typing.cmx \
     kernel/mod_subst.cmx pretyping/matching.cmx proofs/logic.cmx \
     library/library.cmx library/libobject.cmx library/libnames.cmx \
     library/lib.cmx kernel/inductive.cmx tactics/hipattern.cmx \
-    tactics/hiddentac.cmx library/global.cmx pretyping/evd.cmx \
-    proofs/evar_refiner.cmx kernel/environ.cmx tactics/dhyp.cmx \
-    kernel/declarations.cmx interp/constrintern.cmx pretyping/clenv.cmx \
-    tactics/btermdn.cmx tactics/auto.cmi 
+    tactics/hiddentac.cmx library/global.cmx interp/genarg.cmx \
+    pretyping/evd.cmx proofs/evar_refiner.cmx kernel/environ.cmx \
+    tactics/dhyp.cmx kernel/declarations.cmx interp/constrintern.cmx \
+    pretyping/clenv.cmx tactics/btermdn.cmx tactics/auto.cmi 
 tactics/autorewrite.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     pretyping/typing.cmi kernel/term.cmi tactics/tactics.cmi \
     tactics/tacticals.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
@@ -2261,25 +2261,27 @@ toplevel/himsg.cmx: lib/util.cmx kernel/type_errors.cmx pretyping/termops.cmx \
 toplevel/line_oriented_parser.cmo: toplevel/line_oriented_parser.cmi 
 toplevel/line_oriented_parser.cmx: toplevel/line_oriented_parser.cmi 
 toplevel/metasyntax.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
-    interp/topconstr.cmi parsing/termast.cmi library/summary.cmi \
-    pretyping/rawterm.cmi parsing/pptactic.cmi interp/ppextend.cmi lib/pp.cmi \
-    parsing/pcoq.cmi lib/options.cmi interp/notation.cmi library/nametab.cmi \
-    kernel/names.cmi library/library.cmi library/libobject.cmi \
-    library/libnames.cmi library/lib.cmi parsing/lexer.cmi library/global.cmi \
-    interp/genarg.cmi parsing/extend.cmi pretyping/evd.cmi \
-    parsing/esyntax.cmi parsing/egrammar.cmi parsing/coqast.cmi \
-    interp/constrintern.cmi interp/constrextern.cmi pretyping/classops.cmi \
-    parsing/ast.cmi toplevel/metasyntax.cmi 
+    interp/topconstr.cmi parsing/termast.cmi tactics/tacinterp.cmi \
+    library/summary.cmi pretyping/rawterm.cmi parsing/pptactic.cmi \
+    interp/ppextend.cmi lib/pp.cmi parsing/pcoq.cmi lib/options.cmi \
+    interp/notation.cmi library/nametab.cmi kernel/names.cmi \
+    library/library.cmi library/libobject.cmi library/libnames.cmi \
+    library/lib.cmi parsing/lexer.cmi library/global.cmi interp/genarg.cmi \
+    parsing/extend.cmi pretyping/evd.cmi parsing/esyntax.cmi \
+    parsing/egrammar.cmi parsing/coqast.cmi interp/constrintern.cmi \
+    interp/constrextern.cmi pretyping/classops.cmi parsing/ast.cmi \
+    toplevel/metasyntax.cmi 
 toplevel/metasyntax.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
-    interp/topconstr.cmx parsing/termast.cmx library/summary.cmx \
-    pretyping/rawterm.cmx parsing/pptactic.cmx interp/ppextend.cmx lib/pp.cmx \
-    parsing/pcoq.cmx lib/options.cmx interp/notation.cmx library/nametab.cmx \
-    kernel/names.cmx library/library.cmx library/libobject.cmx \
-    library/libnames.cmx library/lib.cmx parsing/lexer.cmx library/global.cmx \
-    interp/genarg.cmx parsing/extend.cmx pretyping/evd.cmx \
-    parsing/esyntax.cmx parsing/egrammar.cmx parsing/coqast.cmx \
-    interp/constrintern.cmx interp/constrextern.cmx pretyping/classops.cmx \
-    parsing/ast.cmx toplevel/metasyntax.cmi 
+    interp/topconstr.cmx parsing/termast.cmx tactics/tacinterp.cmx \
+    library/summary.cmx pretyping/rawterm.cmx parsing/pptactic.cmx \
+    interp/ppextend.cmx lib/pp.cmx parsing/pcoq.cmx lib/options.cmx \
+    interp/notation.cmx library/nametab.cmx kernel/names.cmx \
+    library/library.cmx library/libobject.cmx library/libnames.cmx \
+    library/lib.cmx parsing/lexer.cmx library/global.cmx interp/genarg.cmx \
+    parsing/extend.cmx pretyping/evd.cmx parsing/esyntax.cmx \
+    parsing/egrammar.cmx parsing/coqast.cmx interp/constrintern.cmx \
+    interp/constrextern.cmx pretyping/classops.cmx parsing/ast.cmx \
+    toplevel/metasyntax.cmi 
 toplevel/minicoq.cmo: lib/util.cmi kernel/type_errors.cmi kernel/term.cmi \
     kernel/sign.cmi kernel/safe_typing.cmi lib/pp.cmi kernel/names.cmi \
     kernel/inductive.cmi parsing/g_minicoq.cmi toplevel/fhimsg.cmi \