maj

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

1 files changed, 215 insertions, 198 deletions

diff --git a/.depend b/.depend
index ac438fd607..e8e47d253a 100644
--- a/.depend
+++ b/.depend
@@ -9,7 +9,8 @@ interp/constrextern.cmi: kernel/environ.cmi library/impargs.cmi \
 interp/constrintern.cmi: parsing/coqast.cmi kernel/environ.cmi \
     pretyping/evd.cmi library/impargs.cmi library/libnames.cmi \
     kernel/names.cmi pretyping/pattern.cmi pretyping/rawterm.cmi \
-    kernel/sign.cmi kernel/term.cmi interp/topconstr.cmi 
+    kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi \
+    interp/topconstr.cmi 
 interp/coqlib.cmi: library/libnames.cmi kernel/names.cmi library/nametab.cmi \
     pretyping/pattern.cmi kernel/term.cmi 
 interp/genarg.cmi: pretyping/evd.cmi library/libnames.cmi kernel/names.cmi \
@@ -94,7 +95,7 @@ library/libnames.cmi: kernel/names.cmi lib/pp.cmi lib/predicate.cmi \
 library/libobject.cmi: library/libnames.cmi kernel/names.cmi 
 library/library.cmi: library/libnames.cmi library/libobject.cmi \
     kernel/names.cmi lib/pp.cmi lib/system.cmi lib/util.cmi 
-library/nameops.cmi: kernel/names.cmi lib/pp.cmi 
+library/nameops.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
     lib/util.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \
@@ -171,9 +172,9 @@ pretyping/inductiveops.cmi: kernel/declarations.cmi kernel/environ.cmi \
 pretyping/instantiate.cmi: kernel/environ.cmi pretyping/evd.cmi \
     kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
 pretyping/matching.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
-    pretyping/pattern.cmi kernel/term.cmi 
+    pretyping/pattern.cmi kernel/term.cmi pretyping/termops.cmi 
 pretyping/pattern.cmi: kernel/environ.cmi library/libnames.cmi \
-    kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \
+    kernel/names.cmi library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi \
     kernel/sign.cmi kernel/term.cmi 
 pretyping/pretype_errors.cmi: kernel/environ.cmi pretyping/evd.cmi \
     pretyping/inductiveops.cmi kernel/names.cmi lib/pp.cmi \
@@ -191,7 +192,7 @@ pretyping/reductionops.cmi: kernel/closure.cmi kernel/environ.cmi \
     pretyping/evd.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
 pretyping/retyping.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
-    kernel/term.cmi 
+    pretyping/pattern.cmi kernel/term.cmi pretyping/termops.cmi 
 pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi pretyping/evd.cmi \
     kernel/names.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \
     kernel/term.cmi 
@@ -201,7 +202,7 @@ pretyping/typing.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/term.cmi
 proofs/clenv.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
     lib/pp.cmi pretyping/pretyping.cmi proofs/proof_type.cmi \
     pretyping/rawterm.cmi pretyping/reductionops.cmi kernel/sign.cmi \
-    kernel/term.cmi lib/util.cmi 
+    kernel/term.cmi pretyping/termops.cmi lib/util.cmi 
 proofs/evar_refiner.cmi: kernel/environ.cmi pretyping/evd.cmi \
     kernel/names.cmi proofs/proof_type.cmi proofs/refiner.cmi kernel/sign.cmi \
     kernel/term.cmi interp/topconstr.cmi 
@@ -219,12 +220,13 @@ proofs/proof_type.cmi: kernel/environ.cmi pretyping/evd.cmi interp/genarg.cmi \
     pretyping/pattern.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \
     kernel/term.cmi lib/util.cmi 
 proofs/refiner.cmi: pretyping/evd.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi kernel/sign.cmi proofs/tacexpr.cmo kernel/term.cmi 
+    proofs/proof_type.cmi kernel/sign.cmi proofs/tacexpr.cmo kernel/term.cmi \
+    pretyping/termops.cmi 
 proofs/tacmach.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
     lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
     pretyping/rawterm.cmi kernel/reduction.cmi proofs/refiner.cmi \
     kernel/sign.cmi proofs/tacexpr.cmo pretyping/tacred.cmi kernel/term.cmi \
-    interp/topconstr.cmi 
+    pretyping/termops.cmi interp/topconstr.cmi 
 proofs/tactic_debug.cmi: kernel/environ.cmi kernel/names.cmi \
     pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacexpr.cmo \
     kernel/term.cmi 
@@ -255,9 +257,9 @@ tactics/extratactics.cmi: interp/genarg.cmi kernel/names.cmi \
 tactics/hiddentac.cmi: kernel/names.cmi proofs/proof_type.cmi \
     pretyping/rawterm.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
     pretyping/tacred.cmi kernel/term.cmi 
-tactics/hipattern.cmi: pretyping/evd.cmi kernel/names.cmi \
-    pretyping/pattern.cmi proofs/proof_trees.cmi kernel/sign.cmi \
-    kernel/term.cmi lib/util.cmi 
+tactics/hipattern.cmi: interp/coqlib.cmi pretyping/evd.cmi kernel/names.cmi \
+    pretyping/pattern.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi lib/util.cmi 
 tactics/inv.cmi: kernel/names.cmi pretyping/rawterm.cmi proofs/tacmach.cmi \
     kernel/term.cmi 
 tactics/leminv.cmi: kernel/names.cmi proofs/proof_type.cmi \
@@ -270,7 +272,8 @@ tactics/setoid_replace.cmi: kernel/names.cmi proofs/proof_type.cmi \
     kernel/term.cmi interp/topconstr.cmi 
 tactics/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \
     pretyping/evd.cmi interp/genarg.cmi kernel/names.cmi library/nametab.cmi \
-    lib/pp.cmi proofs/proof_type.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
+    pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \
+    pretyping/rawterm.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
     pretyping/tacred.cmi proofs/tactic_debug.cmi kernel/term.cmi \
     interp/topconstr.cmi lib/util.cmi 
 tactics/tacticals.cmi: proofs/clenv.cmi kernel/names.cmi \
@@ -949,35 +952,35 @@ parsing/g_cases.cmx: parsing/g_constr.cmx library/libnames.cmx \
     parsing/pcoq.cmx lib/pp.cmx kernel/term.cmx interp/topconstr.cmx \
     lib/util.cmx 
 parsing/g_constr.cmo: parsing/lexer.cmi library/libnames.cmi kernel/names.cmi \
-    parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi kernel/term.cmi \
-    interp/topconstr.cmi lib/util.cmi 
+    pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \
+    kernel/term.cmi interp/topconstr.cmi lib/util.cmi 
 parsing/g_constr.cmx: parsing/lexer.cmx library/libnames.cmx kernel/names.cmx \
-    parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx kernel/term.cmx \
-    interp/topconstr.cmx lib/util.cmx 
+    pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx \
+    kernel/term.cmx interp/topconstr.cmx lib/util.cmx 
 parsing/g_constrnew.cmo: lib/bignat.cmi parsing/lexer.cmi \
-    library/libnames.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
-    lib/pp.cmi pretyping/rawterm.cmi kernel/term.cmi interp/topconstr.cmi \
-    lib/util.cmi 
+    library/libnames.cmi kernel/names.cmi lib/options.cmi \
+    pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \
+    kernel/term.cmi interp/topconstr.cmi lib/util.cmi 
 parsing/g_constrnew.cmx: lib/bignat.cmx parsing/lexer.cmx \
-    library/libnames.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
-    lib/pp.cmx pretyping/rawterm.cmx kernel/term.cmx interp/topconstr.cmx \
-    lib/util.cmx 
+    library/libnames.cmx kernel/names.cmx lib/options.cmx \
+    pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx \
+    kernel/term.cmx interp/topconstr.cmx lib/util.cmx 
 parsing/g_ltac.cmo: parsing/ast.cmi interp/genarg.cmi library/libnames.cmi \
-    kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \
-    proofs/tacexpr.cmo interp/topconstr.cmi lib/util.cmi \
-    toplevel/vernacexpr.cmo 
+    kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
+    pretyping/rawterm.cmi proofs/tacexpr.cmo interp/topconstr.cmi \
+    lib/util.cmi toplevel/vernacexpr.cmo 
 parsing/g_ltac.cmx: parsing/ast.cmx interp/genarg.cmx library/libnames.cmx \
-    kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx \
-    proofs/tacexpr.cmx interp/topconstr.cmx lib/util.cmx \
-    toplevel/vernacexpr.cmx 
+    kernel/names.cmx pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx \
+    pretyping/rawterm.cmx proofs/tacexpr.cmx interp/topconstr.cmx \
+    lib/util.cmx toplevel/vernacexpr.cmx 
 parsing/g_ltacnew.cmo: parsing/ast.cmi interp/genarg.cmi library/libnames.cmi \
-    kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \
-    proofs/tacexpr.cmo interp/topconstr.cmi lib/util.cmi \
-    toplevel/vernacexpr.cmo 
+    kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
+    pretyping/rawterm.cmi proofs/tacexpr.cmo interp/topconstr.cmi \
+    lib/util.cmi toplevel/vernacexpr.cmo 
 parsing/g_ltacnew.cmx: parsing/ast.cmx interp/genarg.cmx library/libnames.cmx \
-    kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx \
-    proofs/tacexpr.cmx interp/topconstr.cmx lib/util.cmx \
-    toplevel/vernacexpr.cmx 
+    kernel/names.cmx pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx \
+    pretyping/rawterm.cmx proofs/tacexpr.cmx interp/topconstr.cmx \
+    lib/util.cmx toplevel/vernacexpr.cmx 
 parsing/g_minicoq.cmo: kernel/environ.cmi parsing/lexer.cmi kernel/names.cmi \
     lib/pp.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
     parsing/g_minicoq.cmi 
@@ -1053,17 +1056,21 @@ parsing/g_rsyntaxnew.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \
     lib/pp.cmx pretyping/rawterm.cmx interp/symbols.cmx interp/topconstr.cmx \
     lib/util.cmx 
 parsing/g_tactic.cmo: parsing/ast.cmi interp/genarg.cmi parsing/lexer.cmi \
-    kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \
-    proofs/tacexpr.cmo interp/topconstr.cmi lib/util.cmi 
+    kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
+    pretyping/rawterm.cmi proofs/tacexpr.cmo interp/topconstr.cmi \
+    lib/util.cmi 
 parsing/g_tactic.cmx: parsing/ast.cmx interp/genarg.cmx parsing/lexer.cmx \
-    kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx \
-    proofs/tacexpr.cmx interp/topconstr.cmx lib/util.cmx 
+    kernel/names.cmx pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx \
+    pretyping/rawterm.cmx proofs/tacexpr.cmx interp/topconstr.cmx \
+    lib/util.cmx 
 parsing/g_tacticnew.cmo: parsing/ast.cmi interp/genarg.cmi parsing/lexer.cmi \
-    kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \
-    proofs/tacexpr.cmo interp/topconstr.cmi lib/util.cmi 
+    kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
+    pretyping/rawterm.cmi proofs/tacexpr.cmo interp/topconstr.cmi \
+    lib/util.cmi 
 parsing/g_tacticnew.cmx: parsing/ast.cmx interp/genarg.cmx parsing/lexer.cmx \
-    kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx \
-    proofs/tacexpr.cmx interp/topconstr.cmx lib/util.cmx 
+    kernel/names.cmx pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx \
+    pretyping/rawterm.cmx proofs/tacexpr.cmx interp/topconstr.cmx \
+    lib/util.cmx 
 parsing/g_vernac.cmo: parsing/ast.cmi toplevel/class.cmi \
     library/decl_kinds.cmo parsing/g_basevernac.cmo parsing/g_proofs.cmo \
     interp/genarg.cmi library/goptions.cmi kernel/names.cmi lib/options.cmi \
@@ -1122,26 +1129,28 @@ parsing/pcoq.cmx: parsing/ast.cmx parsing/coqast.cmx library/decl_kinds.cmx \
     interp/topconstr.cmx lib/util.cmx parsing/pcoq.cmi 
 parsing/ppconstr.cmo: parsing/ast.cmi lib/bignat.cmi interp/constrextern.cmi \
     parsing/coqast.cmi interp/genarg.cmi library/libnames.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    interp/ppextend.cmi pretyping/rawterm.cmi interp/symbols.cmi \
-    kernel/term.cmi interp/topconstr.cmi lib/util.cmi parsing/ppconstr.cmi 
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi \
+    pretyping/pattern.cmi lib/pp.cmi interp/ppextend.cmi \
+    pretyping/rawterm.cmi interp/symbols.cmi kernel/term.cmi \
+    interp/topconstr.cmi lib/util.cmi parsing/ppconstr.cmi 
 parsing/ppconstr.cmx: parsing/ast.cmx lib/bignat.cmx interp/constrextern.cmx \
     parsing/coqast.cmx interp/genarg.cmx library/libnames.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    interp/ppextend.cmx pretyping/rawterm.cmx interp/symbols.cmx \
-    kernel/term.cmx interp/topconstr.cmx lib/util.cmx parsing/ppconstr.cmi 
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx \
+    pretyping/pattern.cmx lib/pp.cmx interp/ppextend.cmx \
+    pretyping/rawterm.cmx interp/symbols.cmx kernel/term.cmx \
+    interp/topconstr.cmx lib/util.cmx parsing/ppconstr.cmi 
 parsing/pptactic.cmo: kernel/closure.cmi lib/dyn.cmi parsing/egrammar.cmi \
     parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
     library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
-    lib/pp.cmi parsing/ppconstr.cmi parsing/printer.cmi pretyping/rawterm.cmi \
-    proofs/tacexpr.cmo kernel/term.cmi interp/topconstr.cmi lib/util.cmi \
-    parsing/pptactic.cmi 
+    pretyping/pattern.cmi lib/pp.cmi parsing/ppconstr.cmi parsing/printer.cmi \
+    pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi \
+    interp/topconstr.cmi lib/util.cmi parsing/pptactic.cmi 
 parsing/pptactic.cmx: kernel/closure.cmx lib/dyn.cmx parsing/egrammar.cmx \
     parsing/extend.cmx interp/genarg.cmx library/libnames.cmx \
     library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
-    lib/pp.cmx parsing/ppconstr.cmx parsing/printer.cmx pretyping/rawterm.cmx \
-    proofs/tacexpr.cmx kernel/term.cmx interp/topconstr.cmx lib/util.cmx \
-    parsing/pptactic.cmi 
+    pretyping/pattern.cmx lib/pp.cmx parsing/ppconstr.cmx parsing/printer.cmx \
+    pretyping/rawterm.cmx proofs/tacexpr.cmx kernel/term.cmx \
+    interp/topconstr.cmx lib/util.cmx parsing/pptactic.cmi 
 parsing/prettyp.cmo: pretyping/classops.cmi interp/constrextern.cmi \
     kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
     pretyping/evd.cmi library/global.cmi library/impargs.cmi \
@@ -1389,21 +1398,23 @@ pretyping/pretyping.cmo: pretyping/cases.cmi pretyping/classops.cmi \
     kernel/environ.cmi pretyping/evarconv.cmi pretyping/evarutil.cmi \
     pretyping/evd.cmi pretyping/indrec.cmi kernel/inductive.cmi \
     pretyping/inductiveops.cmi pretyping/instantiate.cmi library/libnames.cmi \
-    kernel/names.cmi lib/pp.cmi pretyping/pretype_errors.cmi \
-    pretyping/rawterm.cmi pretyping/recordops.cmi pretyping/reductionops.cmi \
-    pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \
-    pretyping/termops.cmi kernel/type_errors.cmi kernel/typeops.cmi \
-    lib/util.cmi pretyping/pretyping.cmi 
+    kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \
+    pretyping/pretype_errors.cmi pretyping/rawterm.cmi \
+    pretyping/recordops.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
+    kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi \
+    kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
+    pretyping/pretyping.cmi 
 pretyping/pretyping.cmx: pretyping/cases.cmx pretyping/classops.cmx \
     pretyping/coercion.cmx kernel/declarations.cmx lib/dyn.cmx \
     kernel/environ.cmx pretyping/evarconv.cmx pretyping/evarutil.cmx \
     pretyping/evd.cmx pretyping/indrec.cmx kernel/inductive.cmx \
     pretyping/inductiveops.cmx pretyping/instantiate.cmx library/libnames.cmx \
-    kernel/names.cmx lib/pp.cmx pretyping/pretype_errors.cmx \
-    pretyping/rawterm.cmx pretyping/recordops.cmx pretyping/reductionops.cmx \
-    pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
-    pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \
-    lib/util.cmx pretyping/pretyping.cmi 
+    kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \
+    pretyping/pretype_errors.cmx pretyping/rawterm.cmx \
+    pretyping/recordops.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
+    kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
+    kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
+    pretyping/pretyping.cmi 
 pretyping/rawterm.cmo: lib/dyn.cmi library/libnames.cmi kernel/names.cmi \
     library/nametab.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \
     lib/util.cmi pretyping/rawterm.cmi 
@@ -1454,11 +1465,11 @@ pretyping/tacred.cmx: pretyping/cbv.cmx kernel/closure.cmx \
     kernel/names.cmx library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmx \
     pretyping/reductionops.cmx pretyping/retyping.cmx library/summary.cmx \
     kernel/term.cmx pretyping/termops.cmx lib/util.cmx pretyping/tacred.cmi 
-pretyping/termops.cmo: kernel/environ.cmi library/lib.cmi \
+pretyping/termops.cmo: library/declare.cmi kernel/environ.cmi library/lib.cmi \
     library/libnames.cmi library/nameops.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi lib/util.cmi pretyping/termops.cmi 
-pretyping/termops.cmx: kernel/environ.cmx library/lib.cmx \
+pretyping/termops.cmx: library/declare.cmx kernel/environ.cmx library/lib.cmx \
     library/libnames.cmx library/nameops.cmx kernel/names.cmx \
     library/nametab.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/univ.cmx lib/util.cmx pretyping/termops.cmi 
@@ -1473,19 +1484,21 @@ pretyping/typing.cmx: kernel/environ.cmx kernel/inductive.cmx \
 proofs/clenv.cmo: pretyping/coercion.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
     library/global.cmi pretyping/instantiate.cmi proofs/logic.cmi \
-    library/nameops.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
-    pretyping/reductionops.cmi proofs/refiner.cmi pretyping/retyping.cmi \
-    kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi kernel/term.cmi \
-    pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi proofs/clenv.cmi 
+    library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \
+    parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+    pretyping/rawterm.cmi pretyping/reductionops.cmi proofs/refiner.cmi \
+    pretyping/retyping.cmi kernel/sign.cmi proofs/tacexpr.cmo \
+    proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \
+    pretyping/typing.cmi lib/util.cmi proofs/clenv.cmi 
 proofs/clenv.cmx: pretyping/coercion.cmx kernel/environ.cmx \
     proofs/evar_refiner.cmx pretyping/evarutil.cmx pretyping/evd.cmx \
     library/global.cmx pretyping/instantiate.cmx proofs/logic.cmx \
-    library/nameops.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
-    pretyping/reductionops.cmx proofs/refiner.cmx pretyping/retyping.cmx \
-    kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx kernel/term.cmx \
-    pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx proofs/clenv.cmi 
+    library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \
+    parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
+    pretyping/rawterm.cmx pretyping/reductionops.cmx proofs/refiner.cmx \
+    pretyping/retyping.cmx kernel/sign.cmx proofs/tacexpr.cmx \
+    proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
+    pretyping/typing.cmx lib/util.cmx proofs/clenv.cmi 
 proofs/evar_refiner.cmo: interp/constrintern.cmi kernel/environ.cmi \
     pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \
     pretyping/instantiate.cmi proofs/logic.cmi kernel/names.cmi \
@@ -1730,29 +1743,29 @@ tactics/eqdecide.cmx: tactics/auto.cmx toplevel/cerrors.cmx interp/coqlib.cmx \
     kernel/term.cmx lib/util.cmx 
 tactics/equality.cmo: proofs/clenv.cmi interp/coqlib.cmi \
     kernel/declarations.cmi kernel/environ.cmi proofs/evar_refiner.cmi \
-    pretyping/evarutil.cmi tactics/hipattern.cmi pretyping/indrec.cmi \
-    kernel/inductive.cmi pretyping/inductiveops.cmi pretyping/instantiate.cmi \
-    proofs/logic.cmi pretyping/matching.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 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 \
+    pretyping/evarconv.cmi pretyping/evarutil.cmi tactics/hipattern.cmi \
+    pretyping/indrec.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \
+    pretyping/instantiate.cmi proofs/logic.cmi pretyping/matching.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 \
+    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 \
-    kernel/inductive.cmx pretyping/inductiveops.cmx pretyping/instantiate.cmx \
-    proofs/logic.cmx pretyping/matching.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 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 \
+    pretyping/evarconv.cmx pretyping/evarutil.cmx tactics/hipattern.cmx \
+    pretyping/indrec.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \
+    pretyping/instantiate.cmx proofs/logic.cmx pretyping/matching.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 \
+    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/pptactic.cmi \
@@ -1788,34 +1801,36 @@ tactics/hipattern.cmo: proofs/clenv.cmi interp/coqlib.cmi \
     kernel/declarations.cmi kernel/environ.cmi pretyping/evd.cmi \
     library/global.cmi pretyping/inductiveops.cmi pretyping/matching.cmi \
     library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \
-    proofs/proof_trees.cmi pretyping/reductionops.cmi kernel/term.cmi \
-    pretyping/termops.cmi lib/util.cmi tactics/hipattern.cmi 
+    proofs/proof_trees.cmi pretyping/reductionops.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
+    tactics/hipattern.cmi 
 tactics/hipattern.cmx: proofs/clenv.cmx interp/coqlib.cmx \
     kernel/declarations.cmx kernel/environ.cmx pretyping/evd.cmx \
     library/global.cmx pretyping/inductiveops.cmx pretyping/matching.cmx \
     library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \
-    proofs/proof_trees.cmx pretyping/reductionops.cmx kernel/term.cmx \
-    pretyping/termops.cmx lib/util.cmx tactics/hipattern.cmi 
+    proofs/proof_trees.cmx pretyping/reductionops.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
+    tactics/hipattern.cmi 
 tactics/inv.cmo: proofs/clenv.cmi interp/coqlib.cmi tactics/elim.cmi \
     kernel/environ.cmi tactics/equality.cmi proofs/evar_refiner.cmi \
-    library/global.cmi pretyping/inductiveops.cmi pretyping/matching.cmi \
-    library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \
-    parsing/printer.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
-    kernel/reduction.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
-    kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
-    pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
-    tactics/wcclausenv.cmi tactics/inv.cmi 
+    library/global.cmi tactics/hipattern.cmi pretyping/inductiveops.cmi \
+    pretyping/matching.cmi library/nameops.cmi kernel/names.cmi \
+    pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \
+    proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
+    pretyping/reductionops.cmi pretyping/retyping.cmi kernel/sign.cmi \
+    proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \
+    pretyping/typing.cmi lib/util.cmi tactics/wcclausenv.cmi tactics/inv.cmi 
 tactics/inv.cmx: proofs/clenv.cmx interp/coqlib.cmx tactics/elim.cmx \
     kernel/environ.cmx tactics/equality.cmx proofs/evar_refiner.cmx \
-    library/global.cmx pretyping/inductiveops.cmx pretyping/matching.cmx \
-    library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \
-    parsing/printer.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
-    kernel/reduction.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
-    kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
-    pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
-    tactics/wcclausenv.cmx tactics/inv.cmi 
+    library/global.cmx tactics/hipattern.cmx pretyping/inductiveops.cmx \
+    pretyping/matching.cmx library/nameops.cmx kernel/names.cmx \
+    pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \
+    proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
+    pretyping/reductionops.cmx pretyping/retyping.cmx kernel/sign.cmx \
+    proofs/tacexpr.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \
+    pretyping/typing.cmx lib/util.cmx tactics/wcclausenv.cmx tactics/inv.cmi 
 tactics/leminv.cmo: proofs/clenv.cmi interp/constrintern.cmi \
     library/decl_kinds.cmo kernel/declarations.cmi library/declare.cmi \
     kernel/entries.cmi kernel/environ.cmi proofs/evar_refiner.cmi \
@@ -2286,18 +2301,18 @@ translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \
     interp/constrextern.cmi interp/constrintern.cmi parsing/coqast.cmi \
     pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
     library/libnames.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi lib/pp.cmi interp/ppextend.cmi \
-    pretyping/rawterm.cmi interp/reserve.cmi interp/symbols.cmi \
-    kernel/term.cmi pretyping/termops.cmi interp/topconstr.cmi lib/util.cmi \
-    translate/ppconstrnew.cmi 
+    library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \
+    interp/ppextend.cmi pretyping/rawterm.cmi interp/reserve.cmi \
+    interp/symbols.cmi kernel/term.cmi pretyping/termops.cmi \
+    interp/topconstr.cmi lib/util.cmi translate/ppconstrnew.cmi 
 translate/ppconstrnew.cmx: parsing/ast.cmx lib/bignat.cmx \
     interp/constrextern.cmx interp/constrintern.cmx parsing/coqast.cmx \
     pretyping/evd.cmx interp/genarg.cmx library/global.cmx \
     library/libnames.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx lib/pp.cmx interp/ppextend.cmx \
-    pretyping/rawterm.cmx interp/reserve.cmx interp/symbols.cmx \
-    kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx \
-    translate/ppconstrnew.cmi 
+    library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \
+    interp/ppextend.cmx pretyping/rawterm.cmx interp/reserve.cmx \
+    interp/symbols.cmx kernel/term.cmx pretyping/termops.cmx \
+    interp/topconstr.cmx lib/util.cmx translate/ppconstrnew.cmi 
 translate/pptacticnew.cmo: kernel/closure.cmi lib/dyn.cmi \
     parsing/egrammar.cmi kernel/environ.cmi parsing/extend.cmi \
     interp/genarg.cmi library/libnames.cmi library/nameops.cmi \
@@ -2452,8 +2467,8 @@ contrib/correctness/pmisc.cmx: library/declare.cmx pretyping/evarutil.cmx \
     kernel/names.cmx lib/options.cmx lib/pp.cmx contrib/correctness/ptype.cmi \
     kernel/term.cmx interp/topconstr.cmx lib/util.cmx \
     contrib/correctness/pmisc.cmi 
-contrib/correctness/pmlize.cmo: interp/coqlib.cmi pretyping/evd.cmi \
-    library/global.cmi pretyping/matching.cmi kernel/names.cmi \
+contrib/correctness/pmlize.cmo: pretyping/evd.cmi library/global.cmi \
+    tactics/hipattern.cmi pretyping/matching.cmi kernel/names.cmi \
     contrib/correctness/past.cmi pretyping/pattern.cmi \
     contrib/correctness/pcicenv.cmi contrib/correctness/peffect.cmi \
     contrib/correctness/penv.cmi contrib/correctness/pmisc.cmi \
@@ -2462,8 +2477,8 @@ contrib/correctness/pmlize.cmo: interp/coqlib.cmi pretyping/evd.cmi \
     contrib/correctness/putil.cmi pretyping/reductionops.cmi kernel/term.cmi \
     parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \
     contrib/correctness/pmlize.cmi 
-contrib/correctness/pmlize.cmx: interp/coqlib.cmx pretyping/evd.cmx \
-    library/global.cmx pretyping/matching.cmx kernel/names.cmx \
+contrib/correctness/pmlize.cmx: pretyping/evd.cmx library/global.cmx \
+    tactics/hipattern.cmx pretyping/matching.cmx kernel/names.cmx \
     contrib/correctness/past.cmi pretyping/pattern.cmx \
     contrib/correctness/pcicenv.cmx contrib/correctness/peffect.cmx \
     contrib/correctness/penv.cmx contrib/correctness/pmisc.cmx \
@@ -2530,36 +2545,36 @@ contrib/correctness/psyntax.cmx: lib/bignat.cmx interp/constrextern.cmx \
     toplevel/vernacinterp.cmx contrib/correctness/psyntax.cmi 
 contrib/correctness/ptactic.cmo: library/decl_kinds.cmo tactics/equality.cmi \
     pretyping/evd.cmi tactics/extratactics.cmi library/global.cmi \
-    library/libnames.cmi library/library.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi contrib/correctness/past.cmi \
-    pretyping/pattern.cmi contrib/correctness/pcic.cmi \
-    contrib/correctness/pdb.cmi contrib/correctness/peffect.cmi \
-    contrib/correctness/penv.cmi contrib/correctness/perror.cmi \
-    proofs/pfedit.cmi contrib/correctness/pmisc.cmi \
-    contrib/correctness/pmlize.cmi contrib/correctness/pmonad.cmi lib/pp.cmi \
-    contrib/correctness/pred.cmi contrib/correctness/prename.cmi \
-    pretyping/pretyping.cmi parsing/printer.cmi \
-    contrib/correctness/ptyping.cmi contrib/correctness/putil.cmi \
-    contrib/correctness/pwp.cmi kernel/reduction.cmi proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
-    pretyping/termops.cmi lib/util.cmi toplevel/vernacentries.cmi \
-    contrib/correctness/ptactic.cmi 
+    library/libnames.cmi library/library.cmi library/nameops.cmi \
+    kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    contrib/correctness/past.cmi pretyping/pattern.cmi \
+    contrib/correctness/pcic.cmi contrib/correctness/pdb.cmi \
+    contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/perror.cmi proofs/pfedit.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmlize.cmi \
+    contrib/correctness/pmonad.cmi lib/pp.cmi contrib/correctness/pred.cmi \
+    contrib/correctness/prename.cmi pretyping/pretyping.cmi \
+    parsing/printer.cmi contrib/correctness/ptyping.cmi \
+    contrib/correctness/putil.cmi contrib/correctness/pwp.cmi \
+    kernel/reduction.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
+    toplevel/vernacentries.cmi contrib/correctness/ptactic.cmi 
 contrib/correctness/ptactic.cmx: library/decl_kinds.cmx tactics/equality.cmx \
     pretyping/evd.cmx tactics/extratactics.cmx library/global.cmx \
-    library/libnames.cmx library/library.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx contrib/correctness/past.cmi \
-    pretyping/pattern.cmx contrib/correctness/pcic.cmx \
-    contrib/correctness/pdb.cmx contrib/correctness/peffect.cmx \
-    contrib/correctness/penv.cmx contrib/correctness/perror.cmx \
-    proofs/pfedit.cmx contrib/correctness/pmisc.cmx \
-    contrib/correctness/pmlize.cmx contrib/correctness/pmonad.cmx lib/pp.cmx \
-    contrib/correctness/pred.cmx contrib/correctness/prename.cmx \
-    pretyping/pretyping.cmx parsing/printer.cmx \
-    contrib/correctness/ptyping.cmx contrib/correctness/putil.cmx \
-    contrib/correctness/pwp.cmx kernel/reduction.cmx proofs/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
-    pretyping/termops.cmx lib/util.cmx toplevel/vernacentries.cmx \
-    contrib/correctness/ptactic.cmi 
+    library/libnames.cmx library/library.cmx library/nameops.cmx \
+    kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    contrib/correctness/past.cmi pretyping/pattern.cmx \
+    contrib/correctness/pcic.cmx contrib/correctness/pdb.cmx \
+    contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \
+    contrib/correctness/perror.cmx proofs/pfedit.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmlize.cmx \
+    contrib/correctness/pmonad.cmx lib/pp.cmx contrib/correctness/pred.cmx \
+    contrib/correctness/prename.cmx pretyping/pretyping.cmx \
+    parsing/printer.cmx contrib/correctness/ptyping.cmx \
+    contrib/correctness/putil.cmx contrib/correctness/pwp.cmx \
+    kernel/reduction.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
+    toplevel/vernacentries.cmx contrib/correctness/ptactic.cmi 
 contrib/correctness/ptyping.cmo: interp/constrintern.cmi kernel/environ.cmi \
     pretyping/evd.cmi library/global.cmi toplevel/himsg.cmi kernel/names.cmi \
     contrib/correctness/past.cmi contrib/correctness/pcicenv.cmi \
@@ -2580,38 +2595,40 @@ contrib/correctness/ptyping.cmx: interp/constrintern.cmx kernel/environ.cmx \
     contrib/correctness/putil.cmx pretyping/reductionops.cmx kernel/term.cmx \
     pretyping/termops.cmx interp/topconstr.cmx pretyping/typing.cmx \
     lib/util.cmx contrib/correctness/ptyping.cmi 
-contrib/correctness/putil.cmo: interp/coqlib.cmi kernel/environ.cmi \
-    library/global.cmi pretyping/matching.cmi library/nameops.cmi \
+contrib/correctness/putil.cmo: kernel/environ.cmi library/global.cmi \
+    tactics/hipattern.cmi pretyping/matching.cmi library/nameops.cmi \
     kernel/names.cmi contrib/correctness/past.cmi pretyping/pattern.cmi \
     contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
     contrib/correctness/pmisc.cmi lib/pp.cmi contrib/correctness/prename.cmi \
     parsing/printer.cmi contrib/correctness/ptype.cmi kernel/term.cmi \
     pretyping/termops.cmi lib/util.cmi contrib/correctness/putil.cmi 
-contrib/correctness/putil.cmx: interp/coqlib.cmx kernel/environ.cmx \
-    library/global.cmx pretyping/matching.cmx library/nameops.cmx \
+contrib/correctness/putil.cmx: kernel/environ.cmx library/global.cmx \
+    tactics/hipattern.cmx pretyping/matching.cmx library/nameops.cmx \
     kernel/names.cmx contrib/correctness/past.cmi pretyping/pattern.cmx \
     contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \
     contrib/correctness/pmisc.cmx lib/pp.cmx contrib/correctness/prename.cmx \
     parsing/printer.cmx contrib/correctness/ptype.cmi kernel/term.cmx \
     pretyping/termops.cmx lib/util.cmx contrib/correctness/putil.cmi 
 contrib/correctness/pwp.cmo: kernel/environ.cmi library/global.cmi \
-    library/libnames.cmi kernel/names.cmi library/nametab.cmi \
-    contrib/correctness/past.cmi contrib/correctness/peffect.cmi \
-    contrib/correctness/penv.cmi contrib/correctness/perror.cmi \
-    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
-    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
-    contrib/correctness/ptyping.cmi contrib/correctness/putil.cmi \
-    kernel/reduction.cmi pretyping/reductionops.cmi kernel/term.cmi \
-    pretyping/termops.cmi lib/util.cmi contrib/correctness/pwp.cmi 
+    tactics/hipattern.cmi library/libnames.cmi kernel/names.cmi \
+    library/nametab.cmi contrib/correctness/past.cmi \
+    contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/perror.cmi contrib/correctness/pmisc.cmi \
+    contrib/correctness/pmonad.cmi contrib/correctness/prename.cmi \
+    contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmi \
+    contrib/correctness/putil.cmi kernel/reduction.cmi \
+    pretyping/reductionops.cmi kernel/term.cmi pretyping/termops.cmi \
+    lib/util.cmi contrib/correctness/pwp.cmi 
 contrib/correctness/pwp.cmx: kernel/environ.cmx library/global.cmx \
-    library/libnames.cmx kernel/names.cmx library/nametab.cmx \
-    contrib/correctness/past.cmi contrib/correctness/peffect.cmx \
-    contrib/correctness/penv.cmx contrib/correctness/perror.cmx \
-    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
-    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
-    contrib/correctness/ptyping.cmx contrib/correctness/putil.cmx \
-    kernel/reduction.cmx pretyping/reductionops.cmx kernel/term.cmx \
-    pretyping/termops.cmx lib/util.cmx contrib/correctness/pwp.cmi 
+    tactics/hipattern.cmx library/libnames.cmx kernel/names.cmx \
+    library/nametab.cmx contrib/correctness/past.cmi \
+    contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \
+    contrib/correctness/perror.cmx contrib/correctness/pmisc.cmx \
+    contrib/correctness/pmonad.cmx contrib/correctness/prename.cmx \
+    contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmx \
+    contrib/correctness/putil.cmx kernel/reduction.cmx \
+    pretyping/reductionops.cmx kernel/term.cmx pretyping/termops.cmx \
+    lib/util.cmx contrib/correctness/pwp.cmi 
 contrib/extraction/common.cmo: kernel/declarations.cmi \
     contrib/extraction/extraction.cmi library/global.cmi lib/gset.cmi \
     contrib/extraction/haskell.cmi library/libnames.cmi \
@@ -2806,14 +2823,14 @@ contrib/first-order/sequent.cmx: tactics/auto.cmx interp/constrextern.cmx \
     contrib/first-order/sequent.cmi 
 contrib/first-order/unify.cmo: proofs/clenv.cmi \
     contrib/first-order/formula.cmi library/libnames.cmi kernel/names.cmi \
-    pretyping/reductionops.cmi contrib/first-order/sequent.cmi \
-    proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
-    contrib/first-order/unify.cmi 
+    pretyping/pattern.cmi pretyping/reductionops.cmi \
+    contrib/first-order/sequent.cmi proofs/tacmach.cmi kernel/term.cmi \
+    pretyping/termops.cmi lib/util.cmi contrib/first-order/unify.cmi 
 contrib/first-order/unify.cmx: proofs/clenv.cmx \
     contrib/first-order/formula.cmx library/libnames.cmx kernel/names.cmx \
-    pretyping/reductionops.cmx contrib/first-order/sequent.cmx \
-    proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
-    contrib/first-order/unify.cmi 
+    pretyping/pattern.cmx pretyping/reductionops.cmx \
+    contrib/first-order/sequent.cmx proofs/tacmach.cmx kernel/term.cmx \
+    pretyping/termops.cmx lib/util.cmx contrib/first-order/unify.cmi 
 contrib/fourier/fourierR.cmo: proofs/clenv.cmi tactics/contradiction.cmi \
     interp/coqlib.cmi tactics/equality.cmi contrib/fourier/fourier.cmo \
     library/libnames.cmi library/library.cmi kernel/names.cmi \
@@ -2944,24 +2961,24 @@ contrib/interface/ctast.cmx: parsing/coqast.cmx lib/dyn.cmx \
     library/libnames.cmx kernel/names.cmx lib/util.cmx 
 contrib/interface/dad.cmo: interp/constrextern.cmi interp/constrintern.cmi \
     kernel/environ.cmi pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
-    library/libnames.cmi pretyping/matching.cmi kernel/names.cmi \
-    library/nametab.cmi contrib/interface/paths.cmi pretyping/pattern.cmi \
-    lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
-    pretyping/rawterm.cmi kernel/reduction.cmi proofs/tacexpr.cmo \
-    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
-    kernel/term.cmi interp/topconstr.cmi pretyping/typing.cmi lib/util.cmi \
-    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi \
-    contrib/interface/dad.cmi 
+    library/libnames.cmi pretyping/matching.cmi library/nameops.cmi \
+    kernel/names.cmi library/nametab.cmi contrib/interface/paths.cmi \
+    pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
+    proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi interp/topconstr.cmi \
+    pretyping/typing.cmi lib/util.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi contrib/interface/dad.cmi 
 contrib/interface/dad.cmx: interp/constrextern.cmx interp/constrintern.cmx \
     kernel/environ.cmx pretyping/evd.cmx interp/genarg.cmx library/global.cmx \
-    library/libnames.cmx pretyping/matching.cmx kernel/names.cmx \
-    library/nametab.cmx contrib/interface/paths.cmx pretyping/pattern.cmx \
-    lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
-    pretyping/rawterm.cmx kernel/reduction.cmx proofs/tacexpr.cmx \
-    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
-    kernel/term.cmx interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \
-    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx \
-    contrib/interface/dad.cmi 
+    library/libnames.cmx pretyping/matching.cmx library/nameops.cmx \
+    kernel/names.cmx library/nametab.cmx contrib/interface/paths.cmx \
+    pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
+    proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
+    proofs/tacexpr.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx interp/topconstr.cmx \
+    pretyping/typing.cmx lib/util.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx contrib/interface/dad.cmi 
 contrib/interface/debug_tac.cmo: parsing/ast.cmi toplevel/cerrors.cmi \
     parsing/coqast.cmi interp/genarg.cmi lib/pp.cmi parsing/pptactic.cmi \
     proofs/proof_trees.cmi proofs/proof_type.cmi proofs/refiner.cmi \