maj

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

1 files changed, 26 insertions, 24 deletions

diff --git a/.depend b/.depend
index d6e96b34a8..a1a3a7b0f3 100644
--- a/.depend
+++ b/.depend
@@ -67,8 +67,8 @@ lib/util.cmi: lib/pp.cmi
 library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \
     kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \
     kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \
-    library/library.cmi kernel/names.cmi library/nametab.cmi \
-    kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
+    kernel/names.cmi library/nametab.cmi kernel/safe_typing.cmi \
+    kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 library/declaremods.cmi: kernel/entries.cmi kernel/environ.cmi \
     library/lib.cmi library/libnames.cmi library/libobject.cmi \
     kernel/names.cmi lib/pp.cmi kernel/safe_typing.cmi 
@@ -426,6 +426,8 @@ dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \
     proofs/proof_trees.cmx proofs/refiner.cmx kernel/sign.cmx lib/system.cmx \
     proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \
     pretyping/termops.cmx kernel/univ.cmx 
+doc/parse.cmo: parsing/ast.cmi 
+doc/parse.cmx: parsing/ast.cmx 
 interp/constrextern.cmo: pretyping/classops.cmi library/declare.cmi \
     pretyping/detyping.cmi kernel/environ.cmi library/impargs.cmi \
     kernel/inductive.cmi library/libnames.cmi library/nameops.cmi \
@@ -676,20 +678,20 @@ library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \
     library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \
     library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
     kernel/inductive.cmi library/lib.cmi library/libnames.cmi \
-    library/libobject.cmi library/library.cmi library/nameops.cmi \
-    kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
-    kernel/reduction.cmi kernel/safe_typing.cmi kernel/sign.cmi \
-    library/summary.cmi kernel/term.cmi kernel/type_errors.cmi \
-    kernel/typeops.cmi kernel/univ.cmi lib/util.cmi library/declare.cmi 
+    library/libobject.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/options.cmi lib/pp.cmi kernel/reduction.cmi \
+    kernel/safe_typing.cmi kernel/sign.cmi library/summary.cmi \
+    kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi kernel/univ.cmi \
+    lib/util.cmi library/declare.cmi 
 library/declare.cmx: library/decl_kinds.cmx kernel/declarations.cmx \
     library/dischargedhypsmap.cmx kernel/entries.cmx kernel/environ.cmx \
     library/global.cmx library/impargs.cmx kernel/indtypes.cmx \
     kernel/inductive.cmx library/lib.cmx library/libnames.cmx \
-    library/libobject.cmx library/library.cmx library/nameops.cmx \
-    kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
-    kernel/reduction.cmx kernel/safe_typing.cmx kernel/sign.cmx \
-    library/summary.cmx kernel/term.cmx kernel/type_errors.cmx \
-    kernel/typeops.cmx kernel/univ.cmx lib/util.cmx library/declare.cmi 
+    library/libobject.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/options.cmx lib/pp.cmx kernel/reduction.cmx \
+    kernel/safe_typing.cmx kernel/sign.cmx library/summary.cmx \
+    kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx \
+    lib/util.cmx library/declare.cmi 
 library/declaremods.cmo: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi library/global.cmi library/lib.cmi \
     library/libnames.cmi library/libobject.cmi kernel/modops.cmi \
@@ -1515,12 +1517,12 @@ tactics/equality.cmo: proofs/clenv.cmi interp/coqlib.cmi \
     proofs/logic.cmi library/nameops.cmi kernel/names.cmi \
     pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \
     pretyping/rawterm.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
-    tactics/setoid_replace.cmi kernel/sign.cmi tactics/tacinterp.cmi \
-    proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \
-    kernel/typeops.cmi pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \
-    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi tactics/wcclausenv.cmi \
-    tactics/equality.cmi 
+    tactics/setoid_replace.cmi kernel/sign.cmi proofs/tacexpr.cmo \
+    tactics/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+    pretyping/termops.cmi kernel/typeops.cmi pretyping/typing.cmi \
+    kernel/univ.cmi lib/util.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi tactics/wcclausenv.cmi tactics/equality.cmi 
 tactics/equality.cmx: proofs/clenv.cmx interp/coqlib.cmx \
     kernel/declarations.cmx kernel/environ.cmx proofs/evar_refiner.cmx \
     pretyping/evarutil.cmx tactics/hipattern.cmx pretyping/indrec.cmx \
@@ -1528,12 +1530,12 @@ tactics/equality.cmx: proofs/clenv.cmx interp/coqlib.cmx \
     proofs/logic.cmx library/nameops.cmx kernel/names.cmx \
     pretyping/pattern.cmx lib/pp.cmx proofs/proof_type.cmx \
     pretyping/rawterm.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
-    tactics/setoid_replace.cmx kernel/sign.cmx tactics/tacinterp.cmx \
-    proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \
-    kernel/typeops.cmx pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \
-    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx tactics/wcclausenv.cmx \
-    tactics/equality.cmi 
+    tactics/setoid_replace.cmx kernel/sign.cmx proofs/tacexpr.cmx \
+    tactics/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+    pretyping/termops.cmx kernel/typeops.cmx pretyping/typing.cmx \
+    kernel/univ.cmx lib/util.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx tactics/wcclausenv.cmx tactics/equality.cmi 
 tactics/extraargs.cmo: parsing/extend.cmi interp/genarg.cmi \
     toplevel/metasyntax.cmi parsing/pcoq.cmi lib/pp.cmi parsing/ppconstr.cmi \
     parsing/pptactic.cmi parsing/printer.cmi tactics/tacinterp.cmi \