Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

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

30 files changed, 1421 insertions, 1645 deletions

diff --git a/.depend b/.depend
index f29e747938..1dd798f9a6 100644
--- a/.depend
+++ b/.depend
@@ -33,13 +33,13 @@ library/global.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/indtypes.cmi kernel/names.cmi library/nametab.cmi \
     kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 library/goptions.cmi: kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    kernel/term.cmi 
+    kernel/term.cmi lib/util.cmi 
 library/impargs.cmi: kernel/environ.cmi kernel/names.cmi library/nametab.cmi \
     kernel/term.cmi 
 library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi 
 library/libobject.cmi: kernel/names.cmi 
 library/library.cmi: library/lib.cmi library/libobject.cmi kernel/names.cmi \
-    library/nametab.cmi lib/pp.cmi lib/system.cmi 
+    library/nametab.cmi lib/pp.cmi lib/system.cmi lib/util.cmi 
 library/nameops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/term.cmi 
 library/nametab.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
@@ -48,33 +48,44 @@ library/summary.cmi: kernel/names.cmi
 lib/rtree.cmi: lib/pp.cmi 
 lib/system.cmi: lib/pp.cmi 
 lib/util.cmi: lib/pp.cmi 
-parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
-    parsing/pcoq.cmi lib/pp.cmi 
+parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/genarg.cmi \
+    kernel/names.cmi library/nametab.cmi lib/pp.cmi proofs/tacexpr.cmo \
+    lib/util.cmi 
 parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \
     library/impargs.cmi kernel/names.cmi library/nametab.cmi \
     pretyping/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi \
-    kernel/term.cmi 
+    kernel/term.cmi lib/util.cmi 
 parsing/coqast.cmi: lib/dyn.cmi kernel/names.cmi 
 parsing/coqlib.cmi: kernel/names.cmi library/nametab.cmi \
     pretyping/pattern.cmi kernel/term.cmi 
 parsing/egrammar.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
-    parsing/pcoq.cmi 
+    parsing/genarg.cmi proofs/tacexpr.cmo toplevel/vernacexpr.cmo 
 parsing/esyntax.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
+    kernel/names.cmi lib/pp.cmi toplevel/vernacexpr.cmo 
+parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi library/nametab.cmi \
     lib/pp.cmi 
-parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
-    lib/pp.cmi 
+parsing/genarg.cmi: kernel/closure.cmi parsing/coqast.cmi pretyping/evd.cmi \
+    kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \
+    kernel/term.cmi lib/util.cmi 
 parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/term.cmi 
 parsing/g_zsyntax.cmi: parsing/coqast.cmi 
-parsing/pcoq.cmi: parsing/coqast.cmi 
+parsing/pcoq.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
+    kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \
+    proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo 
+parsing/ppconstr.cmi: parsing/coqast.cmi kernel/environ.cmi \
+    parsing/extend.cmi parsing/genarg.cmi library/nametab.cmi \
+    parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \
+    kernel/term.cmi 
+parsing/pptactic.cmi: parsing/egrammar.cmi parsing/genarg.cmi lib/pp.cmi \
+    proofs/proof_type.cmi proofs/tacexpr.cmo 
 parsing/prettyp.cmi: pretyping/classops.cmi kernel/environ.cmi \
     library/lib.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
     pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+    kernel/term.cmi pretyping/termops.cmi lib/util.cmi 
+parsing/printer.cmi: kernel/environ.cmi kernel/names.cmi library/nametab.cmi \
+    pretyping/pattern.cmi lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi \
     kernel/term.cmi pretyping/termops.cmi 
-parsing/printer.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
-    library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
-    pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \
-    pretyping/termops.cmi 
 parsing/search.cmi: kernel/environ.cmi kernel/names.cmi library/nametab.cmi \
     pretyping/pattern.cmi lib/pp.cmi kernel/term.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
@@ -129,75 +140,91 @@ pretyping/retyping.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
 pretyping/syntax_def.cmi: kernel/names.cmi library/nametab.cmi \
     pretyping/rawterm.cmi 
 pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi pretyping/evd.cmi \
-    kernel/names.cmi pretyping/reductionops.cmi kernel/term.cmi 
+    kernel/names.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \
+    kernel/term.cmi 
 pretyping/termops.cmi: kernel/environ.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi lib/util.cmi 
 pretyping/typing.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/term.cmi 
 proofs/clenv.cmi: kernel/environ.cmi proofs/evar_refiner.cmi \
     pretyping/evd.cmi kernel/names.cmi lib/pp.cmi pretyping/pretyping.cmi \
-    proofs/proof_type.cmi pretyping/reductionops.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi 
+    proofs/proof_type.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi lib/util.cmi 
 proofs/evar_refiner.cmi: parsing/coqast.cmi kernel/environ.cmi \
     pretyping/evd.cmi kernel/names.cmi proofs/proof_type.cmi \
     proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi 
 proofs/logic.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
     lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi 
-proofs/pfedit.cmi: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
-    pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \
+proofs/pfedit.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \
+    kernel/names.cmi library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi \
     kernel/safe_typing.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi 
-proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi \
-    pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \
-    kernel/sign.cmi kernel/term.cmi lib/util.cmi 
-proofs/proof_type.cmi: parsing/coqast.cmi kernel/environ.cmi \
-    pretyping/evd.cmi kernel/names.cmi library/nametab.cmi \
-    pretyping/pretyping.cmi pretyping/tacred.cmi kernel/term.cmi lib/util.cmi 
+proofs/proof_trees.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
+    lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi \
+    lib/util.cmi 
+proofs/proof_type.cmi: kernel/closure.cmi kernel/environ.cmi \
+    pretyping/evd.cmi parsing/genarg.cmi kernel/names.cmi library/nametab.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 kernel/term.cmi 
-proofs/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \
-    pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \
-    proofs/tacmach.cmi proofs/tactic_debug.cmi kernel/term.cmi 
+    proofs/proof_type.cmi kernel/sign.cmi proofs/tacexpr.cmo kernel/term.cmi 
 proofs/tacmach.cmi: kernel/closure.cmi parsing/coqast.cmi kernel/environ.cmi \
-    pretyping/evd.cmi kernel/names.cmi lib/pp.cmi pretyping/pretyping.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
-    proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi 
-proofs/tactic_debug.cmi: parsing/coqast.cmi kernel/environ.cmi \
-    proofs/proof_type.cmi kernel/term.cmi 
-tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi parsing/coqast.cmi \
-    kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi library/nametab.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 
+proofs/tactic_debug.cmi: kernel/environ.cmi kernel/names.cmi \
+    proofs/proof_type.cmi proofs/tacexpr.cmo kernel/term.cmi 
+tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi kernel/environ.cmi \
+    pretyping/evd.cmi kernel/names.cmi library/nametab.cmi \
     pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \
-    pretyping/rawterm.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \
-    lib/util.cmi 
-tactics/autorewrite.cmi: parsing/coqast.cmi proofs/tacmach.cmi \
+    pretyping/rawterm.cmi kernel/sign.cmi proofs/tacexpr.cmo \
+    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo 
+tactics/autorewrite.cmi: proofs/tacexpr.cmo proofs/tacmach.cmi \
     kernel/term.cmi 
 tactics/btermdn.cmi: pretyping/pattern.cmi kernel/term.cmi 
-tactics/dhyp.cmi: kernel/names.cmi proofs/tacmach.cmi 
-tactics/elim.cmi: kernel/names.cmi proofs/proof_type.cmi proofs/tacmach.cmi \
+tactics/contradiction.cmi: kernel/names.cmi proofs/proof_type.cmi \
+    kernel/term.cmi 
+tactics/dhyp.cmi: parsing/genarg.cmi kernel/names.cmi proofs/tacexpr.cmo \
+    proofs/tacmach.cmi 
+tactics/elim.cmi: kernel/names.cmi proofs/proof_type.cmi \
+    pretyping/rawterm.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
     tactics/tacticals.cmi kernel/term.cmi 
 tactics/equality.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \
     tactics/hipattern.cmi kernel/names.cmi pretyping/pattern.cmi \
-    proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
-    tactics/wcclausenv.cmi 
+    proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+    proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi tactics/wcclausenv.cmi 
+tactics/extraargs.cmi: parsing/coqast.cmi parsing/pcoq.cmi \
+    proofs/proof_type.cmi proofs/tacexpr.cmo kernel/term.cmi 
+tactics/extratactics.cmi: parsing/genarg.cmi kernel/names.cmi \
+    proofs/proof_type.cmi kernel/term.cmi 
 tactics/hiddentac.cmi: kernel/names.cmi proofs/proof_type.cmi \
-    tactics/tacentries.cmi proofs/tacmach.cmi kernel/term.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/inv.cmi: kernel/names.cmi proofs/tacmach.cmi kernel/term.cmi 
+tactics/inv.cmi: kernel/names.cmi pretyping/rawterm.cmi proofs/tacmach.cmi \
+    kernel/term.cmi 
+tactics/leminv.cmi: parsing/coqast.cmi kernel/names.cmi proofs/proof_type.cmi \
+    pretyping/rawterm.cmi kernel/term.cmi 
 tactics/nbtermdn.cmi: tactics/btermdn.cmi pretyping/pattern.cmi \
     kernel/term.cmi 
 tactics/refine.cmi: pretyping/pretyping.cmi proofs/tacmach.cmi \
     kernel/term.cmi 
-tactics/setoid_replace.cmi: proofs/proof_type.cmi kernel/term.cmi 
-tactics/tacentries.cmi: proofs/proof_type.cmi proofs/tacmach.cmi 
-tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/names.cmi \
+tactics/setoid_replace.cmi: parsing/genarg.cmi kernel/names.cmi \
+    proofs/proof_type.cmi kernel/term.cmi 
+tactics/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \
+    pretyping/evd.cmi parsing/genarg.cmi kernel/names.cmi lib/pp.cmi \
+    proofs/proof_type.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
+    pretyping/tacred.cmi proofs/tactic_debug.cmi kernel/term.cmi lib/util.cmi 
+tactics/tacticals.cmi: proofs/clenv.cmi kernel/names.cmi \
     pretyping/pattern.cmi proofs/proof_type.cmi kernel/reduction.cmi \
     kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi 
-tactics/tactics.cmi: proofs/clenv.cmi kernel/closure.cmi kernel/environ.cmi \
-    proofs/evar_refiner.cmi pretyping/evd.cmi kernel/names.cmi \
-    library/nametab.cmi proofs/proof_type.cmi kernel/reduction.cmi \
-    kernel/sign.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
+tactics/tactics.cmi: proofs/clenv.cmi kernel/closure.cmi parsing/coqast.cmi \
+    kernel/environ.cmi proofs/evar_refiner.cmi pretyping/evd.cmi \
+    kernel/names.cmi library/nametab.cmi proofs/proof_type.cmi \
+    pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \
+    proofs/tacexpr.cmo proofs/tacmach.cmi pretyping/tacred.cmi \
     tactics/tacticals.cmi kernel/term.cmi 
 tactics/termdn.cmi: pretyping/pattern.cmi kernel/term.cmi 
 tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi \
@@ -205,11 +232,12 @@ tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi \
     proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi 
 toplevel/cerrors.cmi: parsing/coqast.cmi lib/pp.cmi 
 toplevel/class.cmi: pretyping/classops.cmi library/declare.cmi \
-    kernel/names.cmi library/nametab.cmi kernel/term.cmi 
-toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi \
-    kernel/environ.cmi pretyping/evd.cmi kernel/indtypes.cmi \
-    library/library.cmi kernel/names.cmi library/nametab.cmi \
-    kernel/safe_typing.cmi pretyping/tacred.cmi kernel/term.cmi 
+    kernel/names.cmi library/nametab.cmi proofs/proof_type.cmi \
+    kernel/term.cmi 
+toplevel/command.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \
+    kernel/indtypes.cmi library/library.cmi kernel/names.cmi \
+    library/nametab.cmi proofs/proof_type.cmi pretyping/tacred.cmi \
+    kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 toplevel/coqinit.cmi: kernel/names.cmi 
 toplevel/discharge.cmi: kernel/names.cmi 
 toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
@@ -217,20 +245,23 @@ toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
 toplevel/himsg.cmi: pretyping/cases.cmi kernel/environ.cmi \
     kernel/indtypes.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/pretype_errors.cmi kernel/type_errors.cmi 
-toplevel/metasyntax.cmi: parsing/coqast.cmi 
+toplevel/metasyntax.cmi: parsing/coqast.cmi parsing/extend.cmi \
+    library/nametab.cmi proofs/tacexpr.cmo lib/util.cmi \
+    toplevel/vernacexpr.cmo 
 toplevel/mltop.cmi: library/libobject.cmi kernel/names.cmi 
 toplevel/protectedtoplevel.cmi: lib/pp.cmi 
-toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/sign.cmi \
-    kernel/term.cmi 
-toplevel/recordobj.cmi: library/nametab.cmi 
+toplevel/record.cmi: parsing/genarg.cmi kernel/names.cmi kernel/sign.cmi \
+    kernel/term.cmi toplevel/vernacexpr.cmo 
+toplevel/recordobj.cmi: library/nametab.cmi proofs/proof_type.cmi 
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
-toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
-    kernel/names.cmi kernel/term.cmi toplevel/vernacinterp.cmi 
-toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
-    library/nametab.cmi proofs/proof_type.cmi 
-toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
+toplevel/vernacentries.cmi: parsing/coqast.cmi kernel/environ.cmi \
+    pretyping/evd.cmi kernel/names.cmi library/nametab.cmi kernel/term.cmi \
+    lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
+toplevel/vernacinterp.cmi: proofs/tacexpr.cmo 
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi \
+    toplevel/vernacexpr.cmo 
 contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \
     contrib/correctness/ptype.cmi kernel/term.cmi 
 contrib/correctness/pcicenv.cmi: kernel/names.cmi \
@@ -278,6 +309,8 @@ contrib/correctness/pwp.cmi: contrib/correctness/peffect.cmi \
 contrib/extraction/common.cmi: contrib/extraction/miniml.cmi \
     contrib/extraction/mlutil.cmi kernel/names.cmi library/nametab.cmi \
     lib/pp.cmi 
+contrib/extraction/extract_env.cmi: parsing/genarg.cmi kernel/names.cmi \
+    library/nametab.cmi lib/util.cmi 
 contrib/extraction/extraction.cmi: kernel/environ.cmi \
     contrib/extraction/miniml.cmi kernel/names.cmi library/nametab.cmi \
     kernel/term.cmi 
@@ -291,16 +324,17 @@ contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi contrib/extraction/table.cmi \
     kernel/term.cmi 
 contrib/extraction/table.cmi: kernel/names.cmi library/nametab.cmi \
-    toplevel/vernacinterp.cmi 
-contrib/interface/blast.cmi: contrib/interface/ctast.cmo \
-    proofs/proof_type.cmi proofs/tacmach.cmi 
-contrib/interface/dad.cmi: contrib/interface/ctast.cmo proofs/proof_type.cmi \
-    proofs/tacmach.cmi 
-contrib/interface/debug_tac.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
+    lib/util.cmi toplevel/vernacinterp.cmi 
+contrib/interface/blast.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \
     proofs/tacmach.cmi 
-contrib/interface/name_to_ast.cmi: parsing/coqast.cmi library/nametab.cmi 
-contrib/interface/pbp.cmi: contrib/interface/ctast.cmo proofs/proof_type.cmi \
+contrib/interface/dad.cmi: contrib/interface/ctast.cmo proofs/proof_type.cmi \
+    proofs/tacexpr.cmo proofs/tacmach.cmi 
+contrib/interface/debug_tac.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \
     proofs/tacmach.cmi 
+contrib/interface/name_to_ast.cmi: parsing/coqast.cmi library/nametab.cmi \
+    toplevel/vernacexpr.cmo 
+contrib/interface/pbp.cmi: kernel/names.cmi proofs/proof_type.cmi \
+    proofs/tacexpr.cmo proofs/tacmach.cmi 
 contrib/interface/showproof.cmi: contrib/interface/ascent.cmi \
     parsing/astterm.cmi proofs/clenv.cmi parsing/coqast.cmi \
     kernel/declarations.cmi kernel/environ.cmi pretyping/evd.cmi \
@@ -314,26 +348,29 @@ contrib/interface/translate.cmi: contrib/interface/ascent.cmi \
     kernel/term.cmi 
 contrib/interface/vtp.cmi: contrib/interface/ascent.cmi 
 contrib/interface/xlate.cmi: contrib/interface/ascent.cmi \
-    contrib/interface/ctast.cmo 
+    contrib/interface/ctast.cmo kernel/names.cmi proofs/tacexpr.cmo \
+    toplevel/vernacexpr.cmo 
 contrib/jprover/jall.cmi: contrib/jprover/jlogic.cmi \
     contrib/jprover/jterm.cmi contrib/jprover/opname.cmi 
 contrib/jprover/jlogic.cmi: contrib/jprover/jterm.cmi 
 contrib/jprover/jterm.cmi: contrib/jprover/opname.cmi 
-contrib/xml/xmlcommand.cmi: kernel/names.cmi library/nametab.cmi 
+contrib/xml/xmlcommand.cmi: kernel/names.cmi library/nametab.cmi lib/util.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
 dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi 
 dev/db_printers.cmx: kernel/names.cmx lib/pp.cmx 
 dev/top_printers.cmo: parsing/ast.cmi toplevel/cerrors.cmi proofs/clenv.cmi \
     kernel/environ.cmi pretyping/evd.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
-    proofs/refiner.cmi kernel/sign.cmi lib/system.cmi proofs/tacmach.cmi \
-    kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi kernel/univ.cmi 
+    library/nametab.cmi lib/pp.cmi parsing/pptactic.cmi parsing/printer.cmi \
+    proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi lib/system.cmi \
+    proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \
+    pretyping/termops.cmi kernel/univ.cmi 
 dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \
     kernel/environ.cmx pretyping/evd.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/pp.cmx parsing/printer.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 
+    library/nametab.cmx lib/pp.cmx parsing/pptactic.cmx parsing/printer.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 
 kernel/closure.cmo: kernel/environ.cmi kernel/esubst.cmi kernel/names.cmi \
     lib/pp.cmi kernel/term.cmi lib/util.cmi kernel/closure.cmi 
 kernel/closure.cmx: kernel/environ.cmx kernel/esubst.cmx kernel/names.cmx \
@@ -534,10 +571,12 @@ lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
 lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
 lib/util.cmo: lib/pp.cmi lib/util.cmi 
 lib/util.cmx: lib/pp.cmx lib/util.cmi 
-parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
-    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi 
-parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx kernel/names.cmx \
-    parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/ast.cmi 
+parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi parsing/genarg.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
+    proofs/tacexpr.cmo lib/util.cmi parsing/ast.cmi 
+parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx parsing/genarg.cmx \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
+    proofs/tacexpr.cmx lib/util.cmx parsing/ast.cmi 
 parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
     lib/dyn.cmi kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
     library/global.cmi library/impargs.cmi library/nameops.cmi \
@@ -565,33 +604,51 @@ parsing/coqlib.cmo: library/declare.cmi kernel/names.cmi library/nametab.cmi \
 parsing/coqlib.cmx: library/declare.cmx kernel/names.cmx library/nametab.cmx \
     pretyping/pattern.cmx kernel/term.cmx lib/util.cmx parsing/coqlib.cmi 
 parsing/egrammar.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
-    parsing/lexer.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi \
+    parsing/genarg.cmi parsing/lexer.cmi parsing/pcoq.cmi lib/pp.cmi \
+    proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo \
     parsing/egrammar.cmi 
 parsing/egrammar.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmx \
-    parsing/lexer.cmx parsing/pcoq.cmx lib/pp.cmx lib/util.cmx \
+    parsing/genarg.cmx parsing/lexer.cmx parsing/pcoq.cmx lib/pp.cmx \
+    proofs/tacexpr.cmx lib/util.cmx toplevel/vernacexpr.cmx \
     parsing/egrammar.cmi 
 parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
-    lib/gmap.cmi lib/gmapl.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
-    parsing/esyntax.cmi 
+    parsing/genarg.cmi library/global.cmi lib/gmap.cmi lib/gmapl.cmi \
+    kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
+    lib/util.cmi toplevel/vernacexpr.cmo parsing/esyntax.cmi 
 parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmx \
-    lib/gmap.cmx lib/gmapl.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
-    parsing/esyntax.cmi 
-parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
-    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi 
-parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
-    parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi 
-parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx 
+    parsing/genarg.cmx library/global.cmx lib/gmap.cmx lib/gmapl.cmx \
+    kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
+    lib/util.cmx toplevel/vernacexpr.cmx parsing/esyntax.cmi 
+parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
+    parsing/lexer.cmi library/nametab.cmi lib/pp.cmi lib/util.cmi \
+    parsing/extend.cmi 
+parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/genarg.cmx \
+    parsing/lexer.cmx library/nametab.cmx lib/pp.cmx lib/util.cmx \
+    parsing/extend.cmi 
+parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi \
+    parsing/extend.cmi library/goptions.cmi parsing/pcoq.cmi lib/pp.cmi \
+    toplevel/vernacexpr.cmo 
+parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx \
+    parsing/extend.cmx library/goptions.cmx parsing/pcoq.cmx lib/pp.cmx \
+    toplevel/vernacexpr.cmx 
 parsing/g_cases.cmo: parsing/coqast.cmi kernel/names.cmi parsing/pcoq.cmi 
 parsing/g_cases.cmx: parsing/coqast.cmx kernel/names.cmx parsing/pcoq.cmx 
 parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \
     parsing/pcoq.cmi 
 parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx kernel/names.cmx \
     parsing/pcoq.cmx 
-parsing/g_ltac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
-    lib/pp.cmi lib/util.cmi 
-parsing/g_ltac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
-    lib/pp.cmx lib/util.cmx 
+parsing/genarg.cmo: parsing/coqast.cmi pretyping/evd.cmi kernel/names.cmi \
+    library/nametab.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \
+    parsing/genarg.cmi 
+parsing/genarg.cmx: parsing/coqast.cmx pretyping/evd.cmx kernel/names.cmx \
+    library/nametab.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \
+    parsing/genarg.cmi 
+parsing/g_ltac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
+    kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \
+    proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo 
+parsing/g_ltac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/genarg.cmx \
+    kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx \
+    proofs/tacexpr.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 
@@ -599,43 +656,75 @@ parsing/g_minicoq.cmx: kernel/environ.cmx parsing/lexer.cmx kernel/names.cmx \
     lib/pp.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
     parsing/g_minicoq.cmi 
 parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    parsing/coqlib.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \
-    lib/pp.cmi parsing/termast.cmi lib/util.cmi parsing/g_natsyntax.cmi 
+    parsing/coqlib.cmi parsing/esyntax.cmi parsing/extend.cmi \
+    kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi parsing/termast.cmi \
+    lib/util.cmi parsing/g_natsyntax.cmi 
 parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    parsing/coqlib.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx \
-    lib/pp.cmx parsing/termast.cmx lib/util.cmx parsing/g_natsyntax.cmi 
-parsing/g_prim.cmo: parsing/coqast.cmi kernel/names.cmi parsing/pcoq.cmi 
-parsing/g_prim.cmx: parsing/coqast.cmx kernel/names.cmx parsing/pcoq.cmx 
-parsing/g_proofs.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \
-    lib/util.cmi 
-parsing/g_proofs.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \
-    lib/util.cmx 
+    parsing/coqlib.cmx parsing/esyntax.cmx parsing/extend.cmx \
+    kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx parsing/termast.cmx \
+    lib/util.cmx parsing/g_natsyntax.cmi 
+parsing/g_prim.cmo: parsing/coqast.cmi kernel/names.cmi library/nametab.cmi \
+    parsing/pcoq.cmi proofs/tacexpr.cmo 
+parsing/g_prim.cmx: parsing/coqast.cmx kernel/names.cmx library/nametab.cmx \
+    parsing/pcoq.cmx proofs/tacexpr.cmx 
+parsing/g_proofs.cmo: parsing/coqast.cmi parsing/genarg.cmi parsing/pcoq.cmi \
+    lib/pp.cmi proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo 
+parsing/g_proofs.cmx: parsing/coqast.cmx parsing/genarg.cmx parsing/pcoq.cmx \
+    lib/pp.cmx proofs/tacexpr.cmx lib/util.cmx toplevel/vernacexpr.cmx 
 parsing/g_rsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
-    parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
-    lib/util.cmi 
-parsing/g_rsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
-    parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx \
-    lib/util.cmx 
-parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+    parsing/esyntax.cmi parsing/extend.cmi kernel/names.cmi parsing/pcoq.cmi \
     lib/pp.cmi lib/util.cmi 
-parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
-    lib/pp.cmx lib/util.cmx 
-parsing/g_vernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
-    lib/pp.cmi lib/util.cmi 
-parsing/g_vernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
+parsing/g_rsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
+    parsing/esyntax.cmx parsing/extend.cmx kernel/names.cmx parsing/pcoq.cmx \
     lib/pp.cmx lib/util.cmx 
+parsing/g_tactic.cmo: parsing/ast.cmi parsing/genarg.cmi kernel/names.cmi \
+    parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \
+    lib/util.cmi 
+parsing/g_tactic.cmx: parsing/ast.cmx parsing/genarg.cmx kernel/names.cmx \
+    parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \
+    lib/util.cmx 
+parsing/g_vernac.cmo: parsing/ast.cmi toplevel/class.cmi parsing/coqast.cmi \
+    library/declare.cmi parsing/genarg.cmi library/goptions.cmi \
+    library/nametab.cmi lib/options.cmi parsing/pcoq.cmi lib/pp.cmi \
+    toplevel/recordobj.cmi lib/util.cmi toplevel/vernacexpr.cmo 
+parsing/g_vernac.cmx: parsing/ast.cmx toplevel/class.cmx parsing/coqast.cmx \
+    library/declare.cmx parsing/genarg.cmx library/goptions.cmx \
+    library/nametab.cmx lib/options.cmx parsing/pcoq.cmx lib/pp.cmx \
+    toplevel/recordobj.cmx lib/util.cmx toplevel/vernacexpr.cmx 
 parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
-    parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
-    lib/util.cmi parsing/g_zsyntax.cmi 
+    parsing/esyntax.cmi parsing/extend.cmi kernel/names.cmi parsing/pcoq.cmi \
+    lib/pp.cmi lib/util.cmi parsing/g_zsyntax.cmi 
 parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
-    parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx \
-    lib/util.cmx parsing/g_zsyntax.cmi 
+    parsing/esyntax.cmx parsing/extend.cmx kernel/names.cmx parsing/pcoq.cmx \
+    lib/pp.cmx lib/util.cmx parsing/g_zsyntax.cmi 
 parsing/lexer.cmo: parsing/lexer.cmi 
 parsing/lexer.cmx: parsing/lexer.cmi 
-parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
-    lib/util.cmi parsing/pcoq.cmi 
-parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
-    lib/util.cmx parsing/pcoq.cmi 
+parsing/pcoq.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
+    parsing/lexer.cmi lib/options.cmi lib/pp.cmi proofs/tacexpr.cmo \
+    lib/util.cmi toplevel/vernacexpr.cmo parsing/pcoq.cmi 
+parsing/pcoq.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/genarg.cmx \
+    parsing/lexer.cmx lib/options.cmx lib/pp.cmx proofs/tacexpr.cmx \
+    lib/util.cmx toplevel/vernacexpr.cmx parsing/pcoq.cmi 
+parsing/ppconstr.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \
+    parsing/esyntax.cmi parsing/extend.cmi parsing/genarg.cmi \
+    library/global.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi parsing/termast.cmi \
+    lib/util.cmi parsing/ppconstr.cmi 
+parsing/ppconstr.cmx: parsing/ast.cmx parsing/coqast.cmx lib/dyn.cmx \
+    parsing/esyntax.cmx parsing/extend.cmx parsing/genarg.cmx \
+    library/global.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmx parsing/termast.cmx \
+    lib/util.cmx parsing/ppconstr.cmi 
+parsing/pptactic.cmo: kernel/closure.cmi lib/dyn.cmi parsing/egrammar.cmi \
+    parsing/extend.cmi parsing/genarg.cmi library/nameops.cmi \
+    kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/ppconstr.cmi \
+    parsing/printer.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo lib/util.cmi \
+    parsing/pptactic.cmi 
+parsing/pptactic.cmx: kernel/closure.cmx lib/dyn.cmx parsing/egrammar.cmx \
+    parsing/extend.cmx parsing/genarg.cmx library/nameops.cmx \
+    kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/ppconstr.cmx \
+    parsing/printer.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx lib/util.cmx \
+    parsing/pptactic.cmi 
 parsing/prettyp.cmo: pretyping/classops.cmi kernel/declarations.cmi \
     library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
     library/global.cmi library/impargs.cmi kernel/inductive.cmi \
@@ -653,19 +742,25 @@ parsing/prettyp.cmx: pretyping/classops.cmx kernel/declarations.cmx \
     kernel/safe_typing.cmx kernel/sign.cmx pretyping/syntax_def.cmx \
     kernel/term.cmx pretyping/termops.cmx lib/util.cmx parsing/prettyp.cmi 
 parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
-    lib/dyn.cmi kernel/environ.cmi parsing/esyntax.cmi parsing/extend.cmi \
-    library/global.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \
-    kernel/sign.cmi kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \
-    lib/util.cmi parsing/printer.cmi 
+    kernel/environ.cmi parsing/extend.cmi library/global.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    pretyping/pattern.cmi lib/pp.cmi parsing/ppconstr.cmi kernel/sign.cmi \
+    kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi lib/util.cmi \
+    parsing/printer.cmi 
 parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
-    lib/dyn.cmx kernel/environ.cmx parsing/esyntax.cmx parsing/extend.cmx \
-    library/global.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \
-    kernel/sign.cmx kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \
-    lib/util.cmx parsing/printer.cmi 
-parsing/q_coqast.cmo: parsing/coqast.cmi kernel/names.cmi parsing/pcoq.cmi 
-parsing/q_coqast.cmx: parsing/coqast.cmx kernel/names.cmx parsing/pcoq.cmx 
+    kernel/environ.cmx parsing/extend.cmx library/global.cmx \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    pretyping/pattern.cmx lib/pp.cmx parsing/ppconstr.cmx kernel/sign.cmx \
+    kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx lib/util.cmx \
+    parsing/printer.cmi 
+parsing/q_coqast.cmo: parsing/coqast.cmi parsing/genarg.cmi kernel/names.cmi \
+    library/nametab.cmi parsing/pcoq.cmi parsing/q_util.cmi \
+    pretyping/rawterm.cmi proofs/tacexpr.cmo 
+parsing/q_coqast.cmx: parsing/coqast.cmx parsing/genarg.cmx kernel/names.cmx \
+    library/nametab.cmx parsing/pcoq.cmx parsing/q_util.cmx \
+    pretyping/rawterm.cmx proofs/tacexpr.cmx 
+parsing/q_util.cmo: parsing/q_util.cmi 
+parsing/q_util.cmx: parsing/q_util.cmi 
 parsing/search.cmo: parsing/astterm.cmi parsing/coqast.cmi parsing/coqlib.cmi \
     kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
     pretyping/evd.cmi library/global.cmi library/libobject.cmi \
@@ -682,6 +777,12 @@ parsing/search.cmx: parsing/astterm.cmx parsing/coqast.cmx parsing/coqlib.cmx \
     pretyping/pretyping.cmx parsing/printer.cmx pretyping/rawterm.cmx \
     pretyping/retyping.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
     parsing/search.cmi 
+parsing/tacextend.cmo: parsing/ast.cmi parsing/genarg.cmi parsing/pcoq.cmi \
+    lib/pp.cmi lib/pp_control.cmi parsing/q_coqast.cmo parsing/q_util.cmi \
+    lib/util.cmi toplevel/vernacexpr.cmo 
+parsing/tacextend.cmx: parsing/ast.cmx parsing/genarg.cmx parsing/pcoq.cmx \
+    lib/pp.cmx lib/pp_control.cmx parsing/q_coqast.cmx parsing/q_util.cmx \
+    lib/util.cmx toplevel/vernacexpr.cmx 
 parsing/termast.cmo: parsing/ast.cmi pretyping/classops.cmi \
     parsing/coqast.cmi library/declare.cmi pretyping/detyping.cmi \
     kernel/environ.cmi library/impargs.cmi kernel/inductive.cmi \
@@ -696,6 +797,12 @@ parsing/termast.cmx: parsing/ast.cmx pretyping/classops.cmx \
     pretyping/pattern.cmx lib/pp.cmx pretyping/rawterm.cmx \
     pretyping/reductionops.cmx kernel/sign.cmx kernel/term.cmx \
     pretyping/termops.cmx kernel/univ.cmx lib/util.cmx parsing/termast.cmi 
+parsing/vernacextend.cmo: parsing/ast.cmi parsing/genarg.cmi parsing/pcoq.cmi \
+    lib/pp.cmi lib/pp_control.cmi parsing/q_coqast.cmo parsing/q_util.cmi \
+    lib/util.cmi toplevel/vernacexpr.cmo 
+parsing/vernacextend.cmx: parsing/ast.cmx parsing/genarg.cmx parsing/pcoq.cmx \
+    lib/pp.cmx lib/pp_control.cmx parsing/q_coqast.cmx parsing/q_util.cmx \
+    lib/util.cmx toplevel/vernacexpr.cmx 
 pretyping/cases.cmo: pretyping/coercion.cmi kernel/declarations.cmi \
     kernel/environ.cmi pretyping/evarconv.cmi pretyping/evarutil.cmi \
     library/global.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \
@@ -719,13 +826,13 @@ pretyping/cbv.cmx: kernel/closure.cmx kernel/environ.cmx kernel/esubst.cmx \
     pretyping/evd.cmx pretyping/instantiate.cmx kernel/names.cmx lib/pp.cmx \
     kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/cbv.cmi 
 pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi \
-    pretyping/evd.cmi library/global.cmi library/lib.cmi \
+    pretyping/evd.cmi library/global.cmi library/goptions.cmi library/lib.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi \
     pretyping/reductionops.cmi library/summary.cmi pretyping/tacred.cmi \
     kernel/term.cmi pretyping/termops.cmi lib/util.cmi pretyping/classops.cmi 
 pretyping/classops.cmx: library/declare.cmx kernel/environ.cmx \
-    pretyping/evd.cmx library/global.cmx library/lib.cmx \
+    pretyping/evd.cmx library/global.cmx library/goptions.cmx library/lib.cmx \
     library/libobject.cmx library/library.cmx kernel/names.cmx \
     library/nametab.cmx lib/options.cmx lib/pp.cmx pretyping/rawterm.cmx \
     pretyping/reductionops.cmx library/summary.cmx pretyping/tacred.cmx \
@@ -900,16 +1007,16 @@ pretyping/tacred.cmo: pretyping/cbv.cmi kernel/closure.cmi \
     kernel/conv_oracle.cmi kernel/declarations.cmi kernel/environ.cmi \
     pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \
     pretyping/instantiate.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/pp.cmi pretyping/reductionops.cmi \
-    library/summary.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
-    pretyping/tacred.cmi 
+    library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi \
+    pretyping/reductionops.cmi pretyping/retyping.cmi library/summary.cmi \
+    kernel/term.cmi pretyping/termops.cmi lib/util.cmi pretyping/tacred.cmi 
 pretyping/tacred.cmx: pretyping/cbv.cmx kernel/closure.cmx \
     kernel/conv_oracle.cmx kernel/declarations.cmx kernel/environ.cmx \
     pretyping/evd.cmx library/global.cmx kernel/inductive.cmx \
     pretyping/instantiate.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/pp.cmx pretyping/reductionops.cmx \
-    library/summary.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
-    pretyping/tacred.cmi 
+    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/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 
@@ -928,30 +1035,32 @@ proofs/clenv.cmo: kernel/environ.cmi proofs/evar_refiner.cmi \
     pretyping/evarutil.cmi pretyping/evd.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/reductionops.cmi proofs/refiner.cmi pretyping/retyping.cmi \
-    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/termops.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: kernel/environ.cmx proofs/evar_refiner.cmx \
     pretyping/evarutil.cmx pretyping/evd.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/reductionops.cmx proofs/refiner.cmx pretyping/retyping.cmx \
-    kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.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: parsing/astterm.cmi kernel/environ.cmi \
     pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \
     pretyping/instantiate.cmi proofs/logic.cmi kernel/names.cmi \
     lib/options.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
     pretyping/reductionops.cmi proofs/refiner.cmi kernel/sign.cmi \
-    pretyping/tacred.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
-    proofs/evar_refiner.cmi 
+    proofs/tacexpr.cmo pretyping/tacred.cmi kernel/term.cmi \
+    pretyping/typing.cmi lib/util.cmi proofs/evar_refiner.cmi 
 proofs/evar_refiner.cmx: parsing/astterm.cmx kernel/environ.cmx \
     pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \
     pretyping/instantiate.cmx proofs/logic.cmx kernel/names.cmx \
     lib/options.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
     pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \
-    pretyping/tacred.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
-    proofs/evar_refiner.cmi 
+    proofs/tacexpr.cmx pretyping/tacred.cmx kernel/term.cmx \
+    pretyping/typing.cmx lib/util.cmx proofs/evar_refiner.cmi 
 proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
     pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \
     kernel/inductive.cmi pretyping/inductiveops.cmi library/nameops.cmi \
@@ -971,229 +1080,257 @@ proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \
 proofs/pfedit.cmo: parsing/astterm.cmi kernel/declarations.cmi \
     library/declare.cmi lib/edit.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi pretyping/evd.cmi library/lib.cmi \
-    library/nameops.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi kernel/safe_typing.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
-    proofs/pfedit.cmi 
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
+    proofs/proof_trees.cmi proofs/proof_type.cmi kernel/safe_typing.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi \
+    lib/util.cmi proofs/pfedit.cmi 
 proofs/pfedit.cmx: parsing/astterm.cmx kernel/declarations.cmx \
     library/declare.cmx lib/edit.cmx kernel/environ.cmx \
     proofs/evar_refiner.cmx pretyping/evd.cmx library/lib.cmx \
-    library/nameops.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx kernel/safe_typing.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
-    proofs/pfedit.cmi 
-proofs/proof_trees.cmo: parsing/ast.cmi kernel/closure.cmi \
-    pretyping/detyping.cmi kernel/environ.cmi pretyping/evarutil.cmi \
-    pretyping/evd.cmi library/global.cmi library/nameops.cmi kernel/names.cmi \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
+    proofs/proof_trees.cmx proofs/proof_type.cmx kernel/safe_typing.cmx \
+    kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx \
+    lib/util.cmx proofs/pfedit.cmi 
+proofs/proof_trees.cmo: kernel/closure.cmi pretyping/detyping.cmi \
+    kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
+    library/global.cmi library/nameops.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \
-    kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi parsing/termast.cmi \
+    kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi \
     pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
     proofs/proof_trees.cmi 
-proofs/proof_trees.cmx: parsing/ast.cmx kernel/closure.cmx \
-    pretyping/detyping.cmx kernel/environ.cmx pretyping/evarutil.cmx \
-    pretyping/evd.cmx library/global.cmx library/nameops.cmx kernel/names.cmx \
+proofs/proof_trees.cmx: kernel/closure.cmx pretyping/detyping.cmx \
+    kernel/environ.cmx pretyping/evarutil.cmx pretyping/evd.cmx \
+    library/global.cmx library/nameops.cmx kernel/names.cmx \
     library/nametab.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \
-    kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx parsing/termast.cmx \
+    kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx \
     pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
     proofs/proof_trees.cmi 
-proofs/proof_type.cmo: parsing/coqast.cmi kernel/environ.cmi \
-    pretyping/evd.cmi kernel/names.cmi library/nametab.cmi \
-    pretyping/pretyping.cmi pretyping/tacred.cmi kernel/term.cmi lib/util.cmi \
+proofs/proof_type.cmo: kernel/closure.cmi kernel/environ.cmi \
+    pretyping/evd.cmi parsing/genarg.cmi kernel/names.cmi library/nametab.cmi \
+    pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi lib/util.cmi \
     proofs/proof_type.cmi 
-proofs/proof_type.cmx: parsing/coqast.cmx kernel/environ.cmx \
-    pretyping/evd.cmx kernel/names.cmx library/nametab.cmx \
-    pretyping/pretyping.cmx pretyping/tacred.cmx kernel/term.cmx lib/util.cmx \
+proofs/proof_type.cmx: kernel/closure.cmx kernel/environ.cmx \
+    pretyping/evd.cmx parsing/genarg.cmx kernel/names.cmx library/nametab.cmx \
+    pretyping/rawterm.cmx proofs/tacexpr.cmx kernel/term.cmx lib/util.cmx \
     proofs/proof_type.cmi 
-proofs/refiner.cmo: parsing/ast.cmi kernel/environ.cmi pretyping/evarutil.cmi \
+proofs/refiner.cmo: kernel/environ.cmi pretyping/evarutil.cmi \
     pretyping/evd.cmi library/global.cmi pretyping/instantiate.cmi \
-    proofs/logic.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi pretyping/reductionops.cmi kernel/sign.cmi \
-    kernel/term.cmi pretyping/termops.cmi kernel/type_errors.cmi lib/util.cmi \
-    proofs/refiner.cmi 
-proofs/refiner.cmx: parsing/ast.cmx kernel/environ.cmx pretyping/evarutil.cmx \
+    proofs/logic.cmi lib/pp.cmi parsing/pptactic.cmi parsing/printer.cmi \
+    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
+    kernel/sign.cmi proofs/tacexpr.cmo kernel/term.cmi pretyping/termops.cmi \
+    kernel/type_errors.cmi lib/util.cmi proofs/refiner.cmi 
+proofs/refiner.cmx: kernel/environ.cmx pretyping/evarutil.cmx \
     pretyping/evd.cmx library/global.cmx pretyping/instantiate.cmx \
-    proofs/logic.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx pretyping/reductionops.cmx kernel/sign.cmx \
-    kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx lib/util.cmx \
-    proofs/refiner.cmi 
-proofs/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \
-    kernel/conv_oracle.cmi parsing/coqast.cmi kernel/declarations.cmi \
-    library/declare.cmi lib/dyn.cmi kernel/environ.cmi pretyping/evd.cmi \
-    library/global.cmi lib/gmap.cmi library/lib.cmi library/libobject.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
-    pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi \
-    pretyping/pretyping.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
-    pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/sign.cmi \
-    library/summary.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
-    proofs/tactic_debug.cmi kernel/term.cmi pretyping/termops.cmi \
-    pretyping/typing.cmi lib/util.cmi proofs/tacinterp.cmi 
-proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \
-    kernel/conv_oracle.cmx parsing/coqast.cmx kernel/declarations.cmx \
-    library/declare.cmx lib/dyn.cmx kernel/environ.cmx pretyping/evd.cmx \
-    library/global.cmx lib/gmap.cmx library/lib.cmx library/libobject.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
-    pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx \
-    pretyping/pretyping.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
-    pretyping/reductionops.cmx kernel/safe_typing.cmx kernel/sign.cmx \
-    library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
-    proofs/tactic_debug.cmx kernel/term.cmx pretyping/termops.cmx \
-    pretyping/typing.cmx lib/util.cmx proofs/tacinterp.cmi 
+    proofs/logic.cmx lib/pp.cmx parsing/pptactic.cmx parsing/printer.cmx \
+    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \
+    kernel/sign.cmx proofs/tacexpr.cmx kernel/term.cmx pretyping/termops.cmx \
+    kernel/type_errors.cmx lib/util.cmx proofs/refiner.cmi 
+proofs/tacexpr.cmo: parsing/coqast.cmi lib/dyn.cmi parsing/genarg.cmi \
+    kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi lib/util.cmi 
+proofs/tacexpr.cmx: parsing/coqast.cmx lib/dyn.cmx parsing/genarg.cmx \
+    kernel/names.cmx library/nametab.cmx pretyping/rawterm.cmx lib/util.cmx 
 proofs/tacmach.cmo: parsing/astterm.cmi library/declare.cmi \
     kernel/environ.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/reductionops.cmi \
-    proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi \
+    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
+    pretyping/reductionops.cmi proofs/refiner.cmi kernel/sign.cmi \
+    proofs/tacexpr.cmo pretyping/tacred.cmi kernel/term.cmi \
     pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
     proofs/tacmach.cmi 
 proofs/tacmach.cmx: parsing/astterm.cmx library/declare.cmx \
     kernel/environ.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/reductionops.cmx \
-    proofs/refiner.cmx kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx \
+    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
+    pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \
+    proofs/tacexpr.cmx pretyping/tacred.cmx kernel/term.cmx \
     pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
     proofs/tacmach.cmi 
-proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/tacmach.cmi proofs/tactic_debug.cmi 
-proofs/tactic_debug.cmx: parsing/ast.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/tacmach.cmx proofs/tactic_debug.cmi 
+proofs/tactic_debug.cmo: parsing/ast.cmi kernel/names.cmi lib/pp.cmi \
+    parsing/pptactic.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+    proofs/tacmach.cmi proofs/tactic_debug.cmi 
+proofs/tactic_debug.cmx: parsing/ast.cmx kernel/names.cmx lib/pp.cmx \
+    parsing/pptactic.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+    proofs/tacmach.cmx proofs/tactic_debug.cmi 
 scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi 
 scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx 
 scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo 
 scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx 
 tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \
-    parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \
-    tactics/dhyp.cmi proofs/evar_refiner.cmi pretyping/evd.cmi \
-    library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \
-    kernel/inductive.cmi library/lib.cmi library/libobject.cmi \
-    library/library.cmi proofs/logic.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi pretyping/pattern.cmi \
-    proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \
-    pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \
-    library/summary.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
-    pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi tactics/auto.cmi 
+    kernel/declarations.cmi library/declare.cmi tactics/dhyp.cmi \
+    proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \
+    tactics/hiddentac.cmi tactics/hipattern.cmi kernel/inductive.cmi \
+    library/lib.cmi library/libobject.cmi library/library.cmi \
+    proofs/logic.cmi library/nameops.cmi kernel/names.cmi library/nametab.cmi \
+    lib/options.cmi pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi \
+    parsing/pptactic.cmi parsing/printer.cmi proofs/proof_type.cmi \
+    pretyping/rawterm.cmi kernel/reduction.cmi proofs/refiner.cmi \
+    kernel/sign.cmi library/summary.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
+    pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
+    toplevel/vernacexpr.cmo tactics/auto.cmi 
 tactics/auto.cmx: parsing/astterm.cmx tactics/btermdn.cmx proofs/clenv.cmx \
-    parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \
-    tactics/dhyp.cmx proofs/evar_refiner.cmx pretyping/evd.cmx \
-    library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \
-    kernel/inductive.cmx library/lib.cmx library/libobject.cmx \
-    library/library.cmx proofs/logic.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx pretyping/pattern.cmx \
-    proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \
-    pretyping/rawterm.cmx kernel/reduction.cmx kernel/sign.cmx \
-    library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
-    pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx tactics/auto.cmi 
-tactics/autorewrite.cmo: parsing/ast.cmi toplevel/command.cmi \
-    parsing/coqast.cmi tactics/equality.cmi tactics/hipattern.cmi \
-    library/lib.cmi library/libobject.cmi kernel/names.cmi lib/pp.cmi \
-    proofs/proof_type.cmi library/summary.cmi proofs/tacinterp.cmi \
-    proofs/tacmach.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \
-    kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    tactics/autorewrite.cmi 
-tactics/autorewrite.cmx: parsing/ast.cmx toplevel/command.cmx \
-    parsing/coqast.cmx tactics/equality.cmx tactics/hipattern.cmx \
-    library/lib.cmx library/libobject.cmx kernel/names.cmx lib/pp.cmx \
-    proofs/proof_type.cmx library/summary.cmx proofs/tacinterp.cmx \
-    proofs/tacmach.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \
-    kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    tactics/autorewrite.cmi 
+    kernel/declarations.cmx library/declare.cmx tactics/dhyp.cmx \
+    proofs/evar_refiner.cmx pretyping/evd.cmx library/global.cmx \
+    tactics/hiddentac.cmx tactics/hipattern.cmx kernel/inductive.cmx \
+    library/lib.cmx library/libobject.cmx library/library.cmx \
+    proofs/logic.cmx library/nameops.cmx kernel/names.cmx library/nametab.cmx \
+    lib/options.cmx pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx \
+    parsing/pptactic.cmx parsing/printer.cmx proofs/proof_type.cmx \
+    pretyping/rawterm.cmx kernel/reduction.cmx proofs/refiner.cmx \
+    kernel/sign.cmx library/summary.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \
+    pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
+    toplevel/vernacexpr.cmx tactics/auto.cmi 
+tactics/autorewrite.cmo: parsing/ast.cmi parsing/coqast.cmi \
+    tactics/equality.cmi tactics/hipattern.cmi library/lib.cmi \
+    library/libobject.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \
+    library/summary.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
+    toplevel/vernacinterp.cmi tactics/autorewrite.cmi 
+tactics/autorewrite.cmx: parsing/ast.cmx parsing/coqast.cmx \
+    tactics/equality.cmx tactics/hipattern.cmx library/lib.cmx \
+    library/libobject.cmx kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx \
+    library/summary.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
+    toplevel/vernacinterp.cmx tactics/autorewrite.cmi 
 tactics/btermdn.cmo: tactics/dn.cmi pretyping/pattern.cmi kernel/term.cmi \
     tactics/termdn.cmi tactics/btermdn.cmi 
 tactics/btermdn.cmx: tactics/dn.cmx pretyping/pattern.cmx kernel/term.cmx \
     tactics/termdn.cmx tactics/btermdn.cmi 
+tactics/contradiction.cmo: parsing/coqlib.cmi tactics/hipattern.cmi \
+    proofs/proof_type.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
+    tactics/contradiction.cmi 
+tactics/contradiction.cmx: parsing/coqlib.cmx tactics/hipattern.cmx \
+    proofs/proof_type.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
+    tactics/contradiction.cmi 
 tactics/dhyp.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \
     parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \
     library/global.cmi library/lib.cmi library/libobject.cmi \
     library/library.cmi kernel/names.cmi tactics/nbtermdn.cmi \
     pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi proofs/proof_type.cmi \
-    pretyping/rawterm.cmi kernel/reduction.cmi library/summary.cmi \
-    proofs/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi tactics/dhyp.cmi 
+    pretyping/rawterm.cmi kernel/reduction.cmi proofs/refiner.cmi \
+    library/summary.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
+    tactics/dhyp.cmi 
 tactics/dhyp.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
     parsing/coqast.cmx kernel/environ.cmx pretyping/evd.cmx \
     library/global.cmx library/lib.cmx library/libobject.cmx \
     library/library.cmx kernel/names.cmx tactics/nbtermdn.cmx \
     pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx proofs/proof_type.cmx \
-    pretyping/rawterm.cmx kernel/reduction.cmx library/summary.cmx \
-    proofs/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx tactics/dhyp.cmi 
+    pretyping/rawterm.cmx kernel/reduction.cmx proofs/refiner.cmx \
+    library/summary.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
+    tactics/dhyp.cmi 
 tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi 
 tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi 
-tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi proofs/evar_refiner.cmi \
-    lib/explore.cmi proofs/logic.cmi library/nameops.cmi kernel/names.cmi \
-    pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
-    kernel/term.cmi pretyping/termops.cmi lib/util.cmi 
-tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx proofs/evar_refiner.cmx \
-    lib/explore.cmx proofs/logic.cmx library/nameops.cmx kernel/names.cmx \
-    pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
-    kernel/term.cmx pretyping/termops.cmx lib/util.cmx 
-tactics/elim.cmo: proofs/clenv.cmi library/declare.cmi kernel/environ.cmi \
-    tactics/hiddentac.cmi tactics/hipattern.cmi pretyping/inductiveops.cmi \
-    kernel/names.cmi library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi \
-    kernel/reduction.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+tactics/eauto.cmo: tactics/auto.cmi toplevel/cerrors.cmi proofs/clenv.cmi \
+    parsing/egrammar.cmi proofs/evar_refiner.cmi lib/explore.cmi \
+    parsing/genarg.cmi proofs/logic.cmi library/nameops.cmi kernel/names.cmi \
+    pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
+    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
+    kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi \
+    tactics/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi 
+tactics/eauto.cmx: tactics/auto.cmx toplevel/cerrors.cmx proofs/clenv.cmx \
+    parsing/egrammar.cmx proofs/evar_refiner.cmx lib/explore.cmx \
+    parsing/genarg.cmx proofs/logic.cmx library/nameops.cmx kernel/names.cmx \
+    pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
+    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
+    kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx \
+    tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx 
+tactics/elim.cmo: proofs/clenv.cmi kernel/environ.cmi tactics/hiddentac.cmi \
+    tactics/hipattern.cmi pretyping/inductiveops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \
+    pretyping/rawterm.cmi kernel/reduction.cmi proofs/refiner.cmi \
+    proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tacticals.cmi \
     tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
     tactics/elim.cmi 
-tactics/elim.cmx: proofs/clenv.cmx library/declare.cmx kernel/environ.cmx \
-    tactics/hiddentac.cmx tactics/hipattern.cmx pretyping/inductiveops.cmx \
-    kernel/names.cmx library/nametab.cmx lib/pp.cmx proofs/proof_type.cmx \
-    kernel/reduction.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+tactics/elim.cmx: proofs/clenv.cmx kernel/environ.cmx tactics/hiddentac.cmx \
+    tactics/hipattern.cmx pretyping/inductiveops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \
+    pretyping/rawterm.cmx kernel/reduction.cmx proofs/refiner.cmx \
+    proofs/tacexpr.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
     tactics/elim.cmi 
-tactics/eqdecide.cmo: tactics/auto.cmi parsing/coqlib.cmi \
-    kernel/declarations.cmi tactics/equality.cmi library/global.cmi \
-    tactics/hiddentac.cmi tactics/hipattern.cmi library/nameops.cmi \
-    kernel/names.cmi pretyping/pattern.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi lib/util.cmi 
-tactics/eqdecide.cmx: tactics/auto.cmx parsing/coqlib.cmx \
-    kernel/declarations.cmx tactics/equality.cmx library/global.cmx \
-    tactics/hiddentac.cmx tactics/hipattern.cmx library/nameops.cmx \
-    kernel/names.cmx pretyping/pattern.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
-tactics/equality.cmo: parsing/astterm.cmi proofs/clenv.cmi parsing/coqast.cmi \
-    parsing/coqlib.cmi kernel/declarations.cmi kernel/environ.cmi \
-    proofs/evar_refiner.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
-    library/global.cmi lib/gmapl.cmi tactics/hipattern.cmi \
+tactics/eqdecide.cmo: tactics/auto.cmi toplevel/cerrors.cmi \
+    parsing/coqlib.cmi kernel/declarations.cmi parsing/egrammar.cmi \
+    tactics/equality.cmi tactics/extratactics.cmi parsing/genarg.cmi \
+    library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \
+    library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi \
+    parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi proofs/proof_trees.cmi \
+    proofs/proof_type.cmi proofs/refiner.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi 
+tactics/eqdecide.cmx: tactics/auto.cmx toplevel/cerrors.cmx \
+    parsing/coqlib.cmx kernel/declarations.cmx parsing/egrammar.cmx \
+    tactics/equality.cmx tactics/extratactics.cmx parsing/genarg.cmx \
+    library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \
+    library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx \
+    parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx proofs/proof_trees.cmx \
+    proofs/proof_type.cmx proofs/refiner.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
+tactics/equality.cmo: proofs/clenv.cmi parsing/coqast.cmi parsing/coqlib.cmi \
+    kernel/declarations.cmi kernel/environ.cmi proofs/evar_refiner.cmi \
+    pretyping/evarutil.cmi lib/gmapl.cmi tactics/hipattern.cmi \
     pretyping/indrec.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \
-    pretyping/instantiate.cmi library/lib.cmi library/libobject.cmi \
-    proofs/logic.cmi library/nameops.cmi kernel/names.cmi \
-    pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \
-    pretyping/reductionops.cmi pretyping/retyping.cmi \
-    tactics/setoid_replace.cmi proofs/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/vernacinterp.cmi tactics/wcclausenv.cmi tactics/equality.cmi 
-tactics/equality.cmx: parsing/astterm.cmx proofs/clenv.cmx parsing/coqast.cmx \
-    parsing/coqlib.cmx kernel/declarations.cmx kernel/environ.cmx \
-    proofs/evar_refiner.cmx pretyping/evarutil.cmx pretyping/evd.cmx \
-    library/global.cmx lib/gmapl.cmx tactics/hipattern.cmx \
+    pretyping/instantiate.cmi library/libobject.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 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 parsing/coqast.cmx parsing/coqlib.cmx \
+    kernel/declarations.cmx kernel/environ.cmx proofs/evar_refiner.cmx \
+    pretyping/evarutil.cmx lib/gmapl.cmx tactics/hipattern.cmx \
     pretyping/indrec.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \
-    pretyping/instantiate.cmx library/lib.cmx library/libobject.cmx \
-    proofs/logic.cmx library/nameops.cmx kernel/names.cmx \
-    pretyping/pattern.cmx lib/pp.cmx proofs/proof_type.cmx \
-    pretyping/reductionops.cmx pretyping/retyping.cmx \
-    tactics/setoid_replace.cmx proofs/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/vernacinterp.cmx tactics/wcclausenv.cmx tactics/equality.cmi 
-tactics/hiddentac.cmo: proofs/proof_type.cmi tactics/tacentries.cmi \
-    proofs/tacmach.cmi kernel/term.cmi tactics/hiddentac.cmi 
-tactics/hiddentac.cmx: proofs/proof_type.cmx tactics/tacentries.cmx \
-    proofs/tacmach.cmx kernel/term.cmx tactics/hiddentac.cmi 
+    pretyping/instantiate.cmx library/libobject.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 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/genarg.cmi toplevel/metasyntax.cmi \
+    parsing/pcoq.cmi lib/pp.cmi parsing/ppconstr.cmi parsing/pptactic.cmi \
+    parsing/printer.cmi tactics/tacinterp.cmi tactics/extraargs.cmi 
+tactics/extraargs.cmx: parsing/genarg.cmx toplevel/metasyntax.cmx \
+    parsing/pcoq.cmx lib/pp.cmx parsing/ppconstr.cmx parsing/pptactic.cmx \
+    parsing/printer.cmx tactics/tacinterp.cmx tactics/extraargs.cmi 
+tactics/extratactics.cmo: parsing/astterm.cmi tactics/autorewrite.cmi \
+    toplevel/cerrors.cmi tactics/contradiction.cmi parsing/coqast.cmi \
+    parsing/egrammar.cmi tactics/equality.cmi pretyping/evd.cmi \
+    tactics/extraargs.cmi parsing/genarg.cmi library/global.cmi \
+    tactics/inv.cmi tactics/leminv.cmi parsing/pcoq.cmi lib/pp.cmi \
+    parsing/pptactic.cmi pretyping/rawterm.cmi tactics/refine.cmi \
+    proofs/refiner.cmi tactics/setoid_replace.cmi proofs/tacexpr.cmo \
+    tactics/tacinterp.cmi kernel/term.cmi toplevel/vernacinterp.cmi \
+    tactics/extratactics.cmi 
+tactics/extratactics.cmx: parsing/astterm.cmx tactics/autorewrite.cmx \
+    toplevel/cerrors.cmx tactics/contradiction.cmx parsing/coqast.cmx \
+    parsing/egrammar.cmx tactics/equality.cmx pretyping/evd.cmx \
+    tactics/extraargs.cmx parsing/genarg.cmx library/global.cmx \
+    tactics/inv.cmx tactics/leminv.cmx parsing/pcoq.cmx lib/pp.cmx \
+    parsing/pptactic.cmx pretyping/rawterm.cmx tactics/refine.cmx \
+    proofs/refiner.cmx tactics/setoid_replace.cmx proofs/tacexpr.cmx \
+    tactics/tacinterp.cmx kernel/term.cmx toplevel/vernacinterp.cmx \
+    tactics/extratactics.cmi 
+tactics/hiddentac.cmo: proofs/evar_refiner.cmi kernel/names.cmi \
+    proofs/proof_type.cmi pretyping/rawterm.cmi proofs/refiner.cmi \
+    proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tactics.cmi kernel/term.cmi \
+    lib/util.cmi tactics/hiddentac.cmi 
+tactics/hiddentac.cmx: proofs/evar_refiner.cmx kernel/names.cmx \
+    proofs/proof_type.cmx pretyping/rawterm.cmx proofs/refiner.cmx \
+    proofs/tacexpr.cmx proofs/tacmach.cmx tactics/tactics.cmx kernel/term.cmx \
+    lib/util.cmx tactics/hiddentac.cmi 
 tactics/hipattern.cmo: proofs/clenv.cmi parsing/coqlib.cmi \
     kernel/declarations.cmi kernel/environ.cmi pretyping/evd.cmi \
     library/global.cmi pretyping/inductiveops.cmi library/nameops.cmi \
@@ -1210,100 +1347,122 @@ tactics/inv.cmo: proofs/clenv.cmi parsing/coqlib.cmi tactics/elim.cmi \
     kernel/environ.cmi tactics/equality.cmi proofs/evar_refiner.cmi \
     library/global.cmi pretyping/inductiveops.cmi library/nameops.cmi \
     kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_type.cmi kernel/reduction.cmi pretyping/reductionops.cmi \
-    pretyping/retyping.cmi kernel/sign.cmi 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 
+    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 parsing/coqlib.cmx tactics/elim.cmx \
     kernel/environ.cmx tactics/equality.cmx proofs/evar_refiner.cmx \
     library/global.cmx pretyping/inductiveops.cmx library/nameops.cmx \
     kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_type.cmx kernel/reduction.cmx pretyping/reductionops.cmx \
-    pretyping/retyping.cmx kernel/sign.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 
+    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: parsing/astterm.cmi proofs/clenv.cmi \
     kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \
     pretyping/inductiveops.cmi tactics/inv.cmi library/nameops.cmi \
-    kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
-    kernel/safe_typing.cmi kernel/sign.cmi proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
-    pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    tactics/wcclausenv.cmi 
+    kernel/names.cmi library/nametab.cmi proofs/pfedit.cmi lib/pp.cmi \
+    parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+    pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
+    toplevel/vernacexpr.cmo tactics/wcclausenv.cmi tactics/leminv.cmi 
 tactics/leminv.cmx: parsing/astterm.cmx proofs/clenv.cmx \
     kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
     proofs/evar_refiner.cmx pretyping/evd.cmx library/global.cmx \
     pretyping/inductiveops.cmx tactics/inv.cmx library/nameops.cmx \
-    kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \
-    kernel/safe_typing.cmx kernel/sign.cmx proofs/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
-    pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    tactics/wcclausenv.cmx 
+    kernel/names.cmx library/nametab.cmx proofs/pfedit.cmx lib/pp.cmx \
+    parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
+    pretyping/reductionops.cmx kernel/safe_typing.cmx kernel/sign.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
+    toplevel/vernacexpr.cmx tactics/wcclausenv.cmx tactics/leminv.cmi 
 tactics/nbtermdn.cmo: tactics/btermdn.cmi lib/gmap.cmi library/libobject.cmi \
     library/library.cmi kernel/names.cmi pretyping/pattern.cmi \
     kernel/term.cmi tactics/termdn.cmi lib/util.cmi tactics/nbtermdn.cmi 
 tactics/nbtermdn.cmx: tactics/btermdn.cmx lib/gmap.cmx library/libobject.cmx \
     library/library.cmx kernel/names.cmx pretyping/pattern.cmx \
     kernel/term.cmx tactics/termdn.cmx lib/util.cmx tactics/nbtermdn.cmi 
-tactics/refine.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/environ.cmi \
-    pretyping/evd.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_type.cmi kernel/reduction.cmi pretyping/retyping.cmi \
-    kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \
-    pretyping/typing.cmi lib/util.cmi tactics/refine.cmi 
-tactics/refine.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/environ.cmx \
-    pretyping/evd.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_type.cmx kernel/reduction.cmx pretyping/retyping.cmx \
-    kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \
-    pretyping/typing.cmx lib/util.cmx tactics/refine.cmi 
+tactics/refine.cmo: proofs/clenv.cmi kernel/environ.cmi pretyping/evd.cmi \
+    kernel/names.cmi lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi \
+    pretyping/retyping.cmi kernel/sign.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+    pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
+    tactics/refine.cmi 
+tactics/refine.cmx: proofs/clenv.cmx kernel/environ.cmx pretyping/evd.cmx \
+    kernel/names.cmx lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx \
+    pretyping/retyping.cmx kernel/sign.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+    pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
+    tactics/refine.cmi 
 tactics/setoid_replace.cmo: parsing/astterm.cmi tactics/auto.cmi \
     toplevel/command.cmi library/declare.cmi kernel/environ.cmi \
     pretyping/evd.cmi library/global.cmi lib/gmap.cmi library/lib.cmi \
     library/libobject.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 pretyping/reductionops.cmi \
-    kernel/safe_typing.cmi library/summary.cmi proofs/tacmach.cmi \
+    library/nametab.cmi lib/options.cmi lib/pp.cmi parsing/printer.cmi \
+    proofs/proof_type.cmi pretyping/reductionops.cmi kernel/safe_typing.cmi \
+    library/summary.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
     tactics/tactics.cmi kernel/term.cmi parsing/termast.cmi \
     pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
-    toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \
-    tactics/setoid_replace.cmi 
+    toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi tactics/setoid_replace.cmi 
 tactics/setoid_replace.cmx: parsing/astterm.cmx tactics/auto.cmx \
     toplevel/command.cmx library/declare.cmx kernel/environ.cmx \
     pretyping/evd.cmx library/global.cmx lib/gmap.cmx library/lib.cmx \
     library/libobject.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 pretyping/reductionops.cmx \
-    kernel/safe_typing.cmx library/summary.cmx proofs/tacmach.cmx \
+    library/nametab.cmx lib/options.cmx lib/pp.cmx parsing/printer.cmx \
+    proofs/proof_type.cmx pretyping/reductionops.cmx kernel/safe_typing.cmx \
+    library/summary.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \
     pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
-    toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \
-    tactics/setoid_replace.cmi 
-tactics/tacentries.cmo: proofs/evar_refiner.cmi proofs/proof_trees.cmi \
-    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
-    tactics/tacentries.cmi 
-tactics/tacentries.cmx: proofs/evar_refiner.cmx proofs/proof_trees.cmx \
-    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
-    tactics/tacentries.cmi 
-tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \
-    kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
-    proofs/evar_refiner.cmi library/global.cmi pretyping/indrec.cmi \
-    kernel/inductive.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \
-    kernel/reduction.cmi kernel/sign.cmi proofs/tacinterp.cmi \
-    proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \
+    toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx tactics/setoid_replace.cmi 
+tactics/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi tactics/auto.cmi \
+    kernel/closure.cmi parsing/coqast.cmi kernel/declarations.cmi \
+    library/declare.cmi tactics/dhyp.cmi lib/dyn.cmi tactics/elim.cmi \
+    kernel/environ.cmi pretyping/evd.cmi parsing/genarg.cmi \
+    library/global.cmi lib/gmap.cmi tactics/hiddentac.cmi library/lib.cmi \
+    library/libobject.cmi proofs/logic.cmi library/nameops.cmi \
+    kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi \
+    pretyping/pretype_errors.cmi pretyping/pretyping.cmi parsing/printer.cmi \
+    proofs/proof_type.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \
+    proofs/refiner.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+    library/summary.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
+    pretyping/tacred.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \
+    kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \
+    pretyping/typing.cmi lib/util.cmi tactics/tacinterp.cmi 
+tactics/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx tactics/auto.cmx \
+    kernel/closure.cmx parsing/coqast.cmx kernel/declarations.cmx \
+    library/declare.cmx tactics/dhyp.cmx lib/dyn.cmx tactics/elim.cmx \
+    kernel/environ.cmx pretyping/evd.cmx parsing/genarg.cmx \
+    library/global.cmx lib/gmap.cmx tactics/hiddentac.cmx library/lib.cmx \
+    library/libobject.cmx proofs/logic.cmx library/nameops.cmx \
+    kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx \
+    pretyping/pretype_errors.cmx pretyping/pretyping.cmx parsing/printer.cmx \
+    proofs/proof_type.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \
+    proofs/refiner.cmx kernel/safe_typing.cmx kernel/sign.cmx \
+    library/summary.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \
+    pretyping/tacred.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \
+    kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \
+    pretyping/typing.cmx lib/util.cmx tactics/tacinterp.cmi 
+tactics/tacticals.cmo: proofs/clenv.cmi kernel/declarations.cmi \
+    library/declare.cmi kernel/environ.cmi proofs/evar_refiner.cmi \
+    library/global.cmi pretyping/indrec.cmi kernel/inductive.cmi \
+    kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi kernel/reduction.cmi \
+    proofs/refiner.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \
     pretyping/termops.cmi lib/util.cmi tactics/wcclausenv.cmi \
     tactics/tacticals.cmi 
-tactics/tacticals.cmx: proofs/clenv.cmx parsing/coqast.cmx \
-    kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
-    proofs/evar_refiner.cmx library/global.cmx pretyping/indrec.cmx \
-    kernel/inductive.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \
-    kernel/reduction.cmx kernel/sign.cmx proofs/tacinterp.cmx \
-    proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \
+tactics/tacticals.cmx: proofs/clenv.cmx kernel/declarations.cmx \
+    library/declare.cmx kernel/environ.cmx proofs/evar_refiner.cmx \
+    library/global.cmx pretyping/indrec.cmx kernel/inductive.cmx \
+    kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx kernel/reduction.cmx \
+    proofs/refiner.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
     pretyping/termops.cmx lib/util.cmx tactics/wcclausenv.cmx \
     tactics/tacticals.cmi 
 tactics/tactics.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/closure.cmi \
@@ -1313,10 +1472,10 @@ tactics/tactics.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/closure.cmi \
     kernel/inductive.cmi pretyping/inductiveops.cmi proofs/logic.cmi \
     library/nameops.cmi kernel/names.cmi library/nametab.cmi \
     proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
-    pretyping/reductionops.cmi proofs/refiner.cmi kernel/safe_typing.cmi \
-    kernel/sign.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
-    pretyping/tacred.cmi tactics/tacticals.cmi kernel/term.cmi \
-    pretyping/termops.cmi lib/util.cmi tactics/tactics.cmi 
+    pretyping/rawterm.cmi pretyping/reductionops.cmi proofs/refiner.cmi \
+    kernel/safe_typing.cmi kernel/sign.cmi proofs/tacexpr.cmo \
+    proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \
+    kernel/term.cmi pretyping/termops.cmi lib/util.cmi tactics/tactics.cmi 
 tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \
     parsing/coqlib.cmx kernel/declarations.cmx library/declare.cmx \
     kernel/environ.cmx proofs/evar_refiner.cmx pretyping/evd.cmx \
@@ -1324,16 +1483,22 @@ tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \
     kernel/inductive.cmx pretyping/inductiveops.cmx proofs/logic.cmx \
     library/nameops.cmx kernel/names.cmx library/nametab.cmx \
     proofs/pfedit.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
-    pretyping/reductionops.cmx proofs/refiner.cmx kernel/safe_typing.cmx \
-    kernel/sign.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
-    pretyping/tacred.cmx tactics/tacticals.cmx kernel/term.cmx \
-    pretyping/termops.cmx lib/util.cmx tactics/tactics.cmi 
-tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \
-    kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \
-    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi lib/util.cmi 
-tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \
-    kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
-    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx lib/util.cmx 
+    pretyping/rawterm.cmx pretyping/reductionops.cmx proofs/refiner.cmx \
+    kernel/safe_typing.cmx kernel/sign.cmx proofs/tacexpr.cmx \
+    proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \
+    kernel/term.cmx pretyping/termops.cmx lib/util.cmx tactics/tactics.cmi 
+tactics/tauto.cmo: parsing/ast.cmi toplevel/cerrors.cmi parsing/coqast.cmi \
+    parsing/egrammar.cmi parsing/genarg.cmi tactics/hipattern.cmi \
+    kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi \
+    parsing/pptactic.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
+    proofs/refiner.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi lib/util.cmi 
+tactics/tauto.cmx: parsing/ast.cmx toplevel/cerrors.cmx parsing/coqast.cmx \
+    parsing/egrammar.cmx parsing/genarg.cmx tactics/hipattern.cmx \
+    kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx \
+    parsing/pptactic.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
+    proofs/refiner.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx lib/util.cmx 
 tactics/termdn.cmo: tactics/dn.cmi library/nameops.cmi kernel/names.cmi \
     library/nametab.cmi pretyping/pattern.cmi pretyping/rawterm.cmi \
     kernel/term.cmi lib/util.cmi tactics/termdn.cmi 
@@ -1343,15 +1508,15 @@ tactics/termdn.cmx: tactics/dn.cmx library/nameops.cmx kernel/names.cmx \
 tactics/wcclausenv.cmo: proofs/clenv.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \
     proofs/logic.cmi library/nameops.cmi kernel/names.cmi lib/pp.cmi \
-    proofs/proof_trees.cmi pretyping/reductionops.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
-    tactics/wcclausenv.cmi 
+    proofs/proof_trees.cmi pretyping/reductionops.cmi proofs/refiner.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \
+    lib/util.cmi tactics/wcclausenv.cmi 
 tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
     proofs/evar_refiner.cmx pretyping/evd.cmx library/global.cmx \
     proofs/logic.cmx library/nameops.cmx kernel/names.cmx lib/pp.cmx \
-    proofs/proof_trees.cmx pretyping/reductionops.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
-    tactics/wcclausenv.cmi 
+    proofs/proof_trees.cmx pretyping/reductionops.cmx proofs/refiner.cmx \
+    kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
+    lib/util.cmx tactics/wcclausenv.cmi 
 tools/coqdep_lexer.cmo: config/coq_config.cmi 
 tools/coqdep_lexer.cmx: config/coq_config.cmx 
 tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
@@ -1363,48 +1528,50 @@ tools/gallina.cmx: tools/gallina_lexer.cmx
 toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
     kernel/indtypes.cmi parsing/lexer.cmi proofs/logic.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi \
-    pretyping/pretype_errors.cmi proofs/tacmach.cmi kernel/type_errors.cmi \
+    pretyping/pretype_errors.cmi proofs/refiner.cmi kernel/type_errors.cmi \
     kernel/univ.cmi lib/util.cmi toplevel/cerrors.cmi 
 toplevel/cerrors.cmx: parsing/ast.cmx pretyping/cases.cmx toplevel/himsg.cmx \
     kernel/indtypes.cmx parsing/lexer.cmx proofs/logic.cmx \
     library/nametab.cmx lib/options.cmx lib/pp.cmx \
-    pretyping/pretype_errors.cmx proofs/tacmach.cmx kernel/type_errors.cmx \
+    pretyping/pretype_errors.cmx proofs/refiner.cmx kernel/type_errors.cmx \
     kernel/univ.cmx lib/util.cmx toplevel/cerrors.cmi 
 toplevel/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \
     library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
     library/global.cmi kernel/inductive.cmi library/lib.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    parsing/printer.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
-    kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \
-    pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    lib/pp.cmi parsing/printer.cmi pretyping/reductionops.cmi \
+    pretyping/retyping.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+    kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
     toplevel/class.cmi 
 toplevel/class.cmx: pretyping/classops.cmx kernel/declarations.cmx \
     library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \
     library/global.cmx kernel/inductive.cmx library/lib.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    parsing/printer.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
-    kernel/safe_typing.cmx kernel/sign.cmx kernel/term.cmx \
-    pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    lib/pp.cmx parsing/printer.cmx pretyping/reductionops.cmx \
+    pretyping/retyping.cmx kernel/safe_typing.cmx kernel/sign.cmx \
+    kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
     toplevel/class.cmi 
-toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
-    kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
-    pretyping/evd.cmi library/global.cmi library/impargs.cmi \
-    pretyping/indrec.cmi kernel/indtypes.cmi kernel/inductive.cmi \
-    library/lib.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 kernel/safe_typing.cmi \
+toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \
+    parsing/coqast.cmi kernel/declarations.cmi library/declare.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/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 toplevel/command.cmi 
-toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
-    kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
-    pretyping/evd.cmx library/global.cmx library/impargs.cmx \
-    pretyping/indrec.cmx kernel/indtypes.cmx kernel/inductive.cmx \
-    library/lib.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 kernel/safe_typing.cmx \
+toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \
+    parsing/coqast.cmx kernel/declarations.cmx library/declare.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/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 toplevel/command.cmi 
@@ -1418,16 +1585,16 @@ toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmx \
     toplevel/coqinit.cmi 
 toplevel/coqtop.cmo: toplevel/cerrors.cmi config/coq_config.cmi \
     toplevel/coqinit.cmi library/lib.cmi library/library.cmi \
-    toplevel/mltop.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi lib/pp.cmi lib/profile.cmi \
-    library/states.cmi lib/system.cmi toplevel/toplevel.cmi \
-    toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi toplevel/coqtop.cmi 
+    toplevel/mltop.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \
+    lib/pp.cmi lib/profile.cmi library/states.cmi lib/system.cmi \
+    toplevel/toplevel.cmi toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi \
+    toplevel/coqtop.cmi 
 toplevel/coqtop.cmx: toplevel/cerrors.cmx config/coq_config.cmx \
     toplevel/coqinit.cmx library/lib.cmx library/library.cmx \
-    toplevel/mltop.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx lib/pp.cmx lib/profile.cmx \
-    library/states.cmx lib/system.cmx toplevel/toplevel.cmx \
-    toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx toplevel/coqtop.cmi 
+    toplevel/mltop.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \
+    lib/pp.cmx lib/profile.cmx library/states.cmx lib/system.cmx \
+    toplevel/toplevel.cmx toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx \
+    toplevel/coqtop.cmi 
 toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \
     kernel/cooking.cmi kernel/declarations.cmi library/declare.cmi \
     kernel/environ.cmi library/global.cmi library/impargs.cmi \
@@ -1456,28 +1623,30 @@ toplevel/himsg.cmo: parsing/ast.cmi pretyping/cases.cmi kernel/environ.cmi \
     library/global.cmi kernel/indtypes.cmi kernel/inductive.cmi \
     proofs/logic.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \
     lib/pp.cmi pretyping/pretype_errors.cmi parsing/printer.cmi \
-    kernel/reduction.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \
+    kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
     pretyping/termops.cmi kernel/type_errors.cmi lib/util.cmi \
     toplevel/himsg.cmi 
 toplevel/himsg.cmx: parsing/ast.cmx pretyping/cases.cmx kernel/environ.cmx \
     library/global.cmx kernel/indtypes.cmx kernel/inductive.cmx \
     proofs/logic.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \
     lib/pp.cmx pretyping/pretype_errors.cmx parsing/printer.cmx \
-    kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
+    kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     pretyping/termops.cmx kernel/type_errors.cmx lib/util.cmx \
     toplevel/himsg.cmi 
 toplevel/line_oriented_parser.cmo: toplevel/line_oriented_parser.cmi 
 toplevel/line_oriented_parser.cmx: toplevel/line_oriented_parser.cmi 
 toplevel/metasyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
     parsing/coqast.cmi parsing/egrammar.cmi parsing/esyntax.cmi \
-    parsing/extend.cmi library/lib.cmi library/libobject.cmi \
-    library/library.cmi parsing/pcoq.cmi lib/pp.cmi library/summary.cmi \
-    lib/util.cmi toplevel/metasyntax.cmi 
+    parsing/extend.cmi parsing/genarg.cmi library/global.cmi library/lib.cmi \
+    library/libobject.cmi library/library.cmi library/nametab.cmi \
+    parsing/pcoq.cmi lib/pp.cmi library/summary.cmi lib/util.cmi \
+    toplevel/vernacexpr.cmo toplevel/metasyntax.cmi 
 toplevel/metasyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
     parsing/coqast.cmx parsing/egrammar.cmx parsing/esyntax.cmx \
-    parsing/extend.cmx library/lib.cmx library/libobject.cmx \
-    library/library.cmx parsing/pcoq.cmx lib/pp.cmx library/summary.cmx \
-    lib/util.cmx toplevel/metasyntax.cmi 
+    parsing/extend.cmx parsing/genarg.cmx library/global.cmx library/lib.cmx \
+    library/libobject.cmx library/library.cmx library/nametab.cmx \
+    parsing/pcoq.cmx lib/pp.cmx library/summary.cmx lib/util.cmx \
+    toplevel/vernacexpr.cmx toplevel/metasyntax.cmi 
 toplevel/minicoq.cmo: kernel/declarations.cmi toplevel/fhimsg.cmi \
     parsing/g_minicoq.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
     kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \
@@ -1494,11 +1663,11 @@ toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \
     lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx toplevel/mltop.cmi 
 toplevel/protectedtoplevel.cmo: toplevel/cerrors.cmi \
     toplevel/line_oriented_parser.cmi parsing/pcoq.cmi lib/pp.cmi \
-    toplevel/vernac.cmi toplevel/vernacinterp.cmi \
+    toplevel/vernac.cmi toplevel/vernacexpr.cmo \
     toplevel/protectedtoplevel.cmi 
 toplevel/protectedtoplevel.cmx: toplevel/cerrors.cmx \
     toplevel/line_oriented_parser.cmx parsing/pcoq.cmx lib/pp.cmx \
-    toplevel/vernac.cmx toplevel/vernacinterp.cmx \
+    toplevel/vernac.cmx toplevel/vernacexpr.cmx \
     toplevel/protectedtoplevel.cmi 
 toplevel/record.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \
     toplevel/command.cmi parsing/coqast.cmi kernel/declarations.cmi \
@@ -1508,7 +1677,7 @@ toplevel/record.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi parsing/printer.cmi \
     pretyping/recordops.cmi kernel/safe_typing.cmi kernel/term.cmi \
     pretyping/termops.cmi kernel/type_errors.cmi kernel/typeops.cmi \
-    lib/util.cmi toplevel/record.cmi 
+    lib/util.cmi toplevel/vernacexpr.cmo toplevel/record.cmi 
 toplevel/record.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \
     toplevel/command.cmx parsing/coqast.cmx kernel/declarations.cmx \
     library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \
@@ -1517,7 +1686,7 @@ toplevel/record.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \
     library/nametab.cmx lib/options.cmx lib/pp.cmx parsing/printer.cmx \
     pretyping/recordops.cmx kernel/safe_typing.cmx kernel/term.cmx \
     pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \
-    lib/util.cmx toplevel/record.cmi 
+    lib/util.cmx toplevel/vernacexpr.cmx toplevel/record.cmi 
 toplevel/recordobj.cmo: pretyping/classops.cmi library/declare.cmi \
     kernel/environ.cmi library/global.cmi pretyping/instantiate.cmi \
     library/lib.cmi library/nameops.cmi kernel/names.cmi library/nametab.cmi \
@@ -1531,67 +1700,75 @@ toplevel/recordobj.cmx: pretyping/classops.cmx library/declare.cmx \
 toplevel/toplevel.cmo: parsing/ast.cmi toplevel/cerrors.cmi library/lib.cmi \
     toplevel/mltop.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
     proofs/pfedit.cmi lib/pp.cmi toplevel/protectedtoplevel.cmi lib/util.cmi \
-    toplevel/vernac.cmi toplevel/vernacinterp.cmi toplevel/toplevel.cmi 
+    toplevel/vernac.cmi toplevel/vernacexpr.cmo toplevel/toplevel.cmi 
 toplevel/toplevel.cmx: parsing/ast.cmx toplevel/cerrors.cmx library/lib.cmx \
     toplevel/mltop.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
     proofs/pfedit.cmx lib/pp.cmx toplevel/protectedtoplevel.cmx lib/util.cmx \
-    toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
+    toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi 
 toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
-    toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \
-    parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \
-    toplevel/discharge.cmi kernel/environ.cmi proofs/evar_refiner.cmi \
-    pretyping/evarutil.cmi pretyping/evd.cmi parsing/extend.cmi \
-    library/global.cmi library/goptions.cmi library/impargs.cmi \
-    pretyping/inductiveops.cmi library/lib.cmi library/library.cmi \
-    toplevel/metasyntax.cmi toplevel/mltop.cmi library/nameops.cmi \
-    kernel/names.cmi library/nametab.cmi lib/options.cmi proofs/pfedit.cmi \
-    lib/pp.cmi lib/pp_control.cmi parsing/prettyp.cmi parsing/printer.cmi \
+    tactics/auto.cmi toplevel/class.cmi pretyping/classops.cmi \
+    toplevel/command.cmi parsing/coqast.cmi library/declare.cmi \
+    tactics/dhyp.cmi toplevel/discharge.cmi kernel/environ.cmi \
+    pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \
+    library/goptions.cmi library/impargs.cmi pretyping/inductiveops.cmi \
+    library/lib.cmi library/library.cmi toplevel/metasyntax.cmi \
+    toplevel/mltop.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \
+    lib/pp_control.cmi parsing/prettyp.cmi parsing/printer.cmi \
     proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \
     toplevel/recordobj.cmi proofs/refiner.cmi kernel/safe_typing.cmi \
     parsing/search.cmi library/states.cmi pretyping/syntax_def.cmi \
-    lib/system.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
+    lib/system.cmi tactics/tacinterp.cmi proofs/tacmach.cmi \
     pretyping/tacred.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \
     kernel/term.cmi parsing/termast.cmi kernel/typeops.cmi kernel/univ.cmi \
-    lib/util.cmi toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
+    lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi \
+    toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
-    toplevel/class.cmx pretyping/classops.cmx toplevel/command.cmx \
-    parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \
-    toplevel/discharge.cmx kernel/environ.cmx proofs/evar_refiner.cmx \
-    pretyping/evarutil.cmx pretyping/evd.cmx parsing/extend.cmx \
-    library/global.cmx library/goptions.cmx library/impargs.cmx \
-    pretyping/inductiveops.cmx library/lib.cmx library/library.cmx \
-    toplevel/metasyntax.cmx toplevel/mltop.cmx library/nameops.cmx \
-    kernel/names.cmx library/nametab.cmx lib/options.cmx proofs/pfedit.cmx \
-    lib/pp.cmx lib/pp_control.cmx parsing/prettyp.cmx parsing/printer.cmx \
+    tactics/auto.cmx toplevel/class.cmx pretyping/classops.cmx \
+    toplevel/command.cmx parsing/coqast.cmx library/declare.cmx \
+    tactics/dhyp.cmx toplevel/discharge.cmx kernel/environ.cmx \
+    pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \
+    library/goptions.cmx library/impargs.cmx pretyping/inductiveops.cmx \
+    library/lib.cmx library/library.cmx toplevel/metasyntax.cmx \
+    toplevel/mltop.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \
+    lib/pp_control.cmx parsing/prettyp.cmx parsing/printer.cmx \
     proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \
     toplevel/recordobj.cmx proofs/refiner.cmx kernel/safe_typing.cmx \
     parsing/search.cmx library/states.cmx pretyping/syntax_def.cmx \
-    lib/system.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
+    lib/system.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \
     pretyping/tacred.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \
     kernel/term.cmx parsing/termast.cmx kernel/typeops.cmx kernel/univ.cmx \
-    lib/util.cmx toplevel/vernacinterp.cmx toplevel/vernacentries.cmi 
-toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi \
-    toplevel/command.cmi parsing/coqast.cmi lib/dyn.cmi toplevel/himsg.cmi \
-    kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
-    proofs/proof_type.cmi proofs/tacinterp.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi 
-toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \
-    toplevel/command.cmx parsing/coqast.cmx lib/dyn.cmx toplevel/himsg.cmx \
-    kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
-    proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmi 
+    lib/util.cmx toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx \
+    toplevel/vernacentries.cmi 
+toplevel/vernacexpr.cmo: parsing/ast.cmi parsing/coqast.cmi \
+    parsing/extend.cmi parsing/genarg.cmi library/goptions.cmi \
+    kernel/names.cmi library/nametab.cmi proofs/proof_type.cmi \
+    proofs/tacexpr.cmo lib/util.cmi 
+toplevel/vernacexpr.cmx: parsing/ast.cmx parsing/coqast.cmx \
+    parsing/extend.cmx parsing/genarg.cmx library/goptions.cmx \
+    kernel/names.cmx library/nametab.cmx proofs/proof_type.cmx \
+    proofs/tacexpr.cmx lib/util.cmx 
+toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi \
+    parsing/extend.cmi toplevel/himsg.cmi kernel/names.cmi lib/options.cmi \
+    lib/pp.cmi proofs/proof_type.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \
+    lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
+toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \
+    parsing/extend.cmx toplevel/himsg.cmx kernel/names.cmx lib/options.cmx \
+    lib/pp.cmx proofs/proof_type.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \
+    lib/util.cmx toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi 
 toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
     library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \
     parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \
-    pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    toplevel/vernac.cmi 
+    pretyping/termops.cmi lib/util.cmi toplevel/vernacentries.cmi \
+    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi 
 toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
     library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \
     parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \
-    pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    toplevel/vernac.cmi 
+    pretyping/termops.cmx lib/util.cmx toplevel/vernacentries.cmx \
+    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
     contrib/correctness/past.cmi contrib/correctness/penv.cmi \
     contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
@@ -1610,14 +1787,14 @@ contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \
     contrib/correctness/past.cmi contrib/correctness/pmisc.cmi \
     pretyping/rawterm.cmi toplevel/record.cmi kernel/sign.cmi kernel/term.cmi \
     pretyping/termops.cmi kernel/typeops.cmi lib/util.cmi \
-    contrib/correctness/pcic.cmi 
+    toplevel/vernacexpr.cmo contrib/correctness/pcic.cmi 
 contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \
     library/declare.cmx pretyping/detyping.cmx library/global.cmx \
     kernel/indtypes.cmx kernel/names.cmx library/nametab.cmx \
     contrib/correctness/past.cmi contrib/correctness/pmisc.cmx \
     pretyping/rawterm.cmx toplevel/record.cmx kernel/sign.cmx kernel/term.cmx \
     pretyping/termops.cmx kernel/typeops.cmx lib/util.cmx \
-    contrib/correctness/pcic.cmi 
+    toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi 
 contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \
     kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
     contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -1725,9 +1902,10 @@ contrib/correctness/prename.cmx: toplevel/himsg.cmx library/nameops.cmx \
     kernel/names.cmx contrib/correctness/pmisc.cmx lib/pp.cmx lib/util.cmx \
     contrib/correctness/prename.cmi 
 contrib/correctness/psyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
-    parsing/coqast.cmi library/declare.cmi lib/dyn.cmi pretyping/evd.cmi \
-    parsing/g_zsyntax.cmi library/global.cmi toplevel/himsg.cmi \
-    library/nameops.cmi kernel/names.cmi lib/options.cmi \
+    parsing/coqast.cmi library/declare.cmi pretyping/evd.cmi \
+    parsing/extend.cmi parsing/g_zsyntax.cmi parsing/genarg.cmi \
+    library/global.cmi toplevel/himsg.cmi library/nameops.cmi \
+    kernel/names.cmi library/nametab.cmi lib/options.cmi \
     contrib/correctness/past.cmi contrib/correctness/pcicenv.cmi \
     parsing/pcoq.cmi contrib/correctness/pdb.cmi \
     contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -1735,13 +1913,14 @@ contrib/correctness/psyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
     contrib/correctness/prename.cmi contrib/correctness/ptactic.cmi \
     contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmi \
     contrib/correctness/putil.cmi kernel/reduction.cmi kernel/safe_typing.cmi \
-    proofs/tacinterp.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \
-    toplevel/vernac.cmi toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \
-    contrib/correctness/psyntax.cmi 
+    tactics/tacinterp.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \
+    toplevel/vernac.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi contrib/correctness/psyntax.cmi 
 contrib/correctness/psyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
-    parsing/coqast.cmx library/declare.cmx lib/dyn.cmx pretyping/evd.cmx \
-    parsing/g_zsyntax.cmx library/global.cmx toplevel/himsg.cmx \
-    library/nameops.cmx kernel/names.cmx lib/options.cmx \
+    parsing/coqast.cmx library/declare.cmx pretyping/evd.cmx \
+    parsing/extend.cmx parsing/g_zsyntax.cmx parsing/genarg.cmx \
+    library/global.cmx toplevel/himsg.cmx library/nameops.cmx \
+    kernel/names.cmx library/nametab.cmx lib/options.cmx \
     contrib/correctness/past.cmi contrib/correctness/pcicenv.cmx \
     parsing/pcoq.cmx contrib/correctness/pdb.cmx \
     contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \
@@ -1749,12 +1928,13 @@ contrib/correctness/psyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
     contrib/correctness/prename.cmx contrib/correctness/ptactic.cmx \
     contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmx \
     contrib/correctness/putil.cmx kernel/reduction.cmx kernel/safe_typing.cmx \
-    proofs/tacinterp.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \
-    toplevel/vernac.cmx toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \
-    contrib/correctness/psyntax.cmi 
-contrib/correctness/ptactic.cmo: library/declare.cmi tactics/equality.cmi \
-    pretyping/evd.cmi library/global.cmi kernel/names.cmi library/nametab.cmi \
-    lib/options.cmi contrib/correctness/past.cmi pretyping/pattern.cmi \
+    tactics/tacinterp.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \
+    toplevel/vernac.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx contrib/correctness/psyntax.cmi 
+contrib/correctness/ptactic.cmo: tactics/equality.cmi pretyping/evd.cmi \
+    tactics/extratactics.cmi library/global.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 \
@@ -1763,13 +1943,13 @@ contrib/correctness/ptactic.cmo: library/declare.cmi tactics/equality.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 tactics/refine.cmi proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
-    pretyping/termops.cmi lib/util.cmi toplevel/vernacentries.cmi \
-    toplevel/vernacinterp.cmi contrib/correctness/ptactic.cmi 
-contrib/correctness/ptactic.cmx: library/declare.cmx tactics/equality.cmx \
-    pretyping/evd.cmx library/global.cmx kernel/names.cmx library/nametab.cmx \
-    lib/options.cmx contrib/correctness/past.cmi pretyping/pattern.cmx \
+    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: tactics/equality.cmx pretyping/evd.cmx \
+    tactics/extratactics.cmx library/global.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 \
@@ -1778,10 +1958,9 @@ contrib/correctness/ptactic.cmx: library/declare.cmx tactics/equality.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 tactics/refine.cmx proofs/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
-    pretyping/termops.cmx lib/util.cmx toplevel/vernacentries.cmx \
-    toplevel/vernacinterp.cmx contrib/correctness/ptactic.cmi 
+    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: parsing/ast.cmi parsing/astterm.cmi \
     kernel/environ.cmi pretyping/evd.cmi library/global.cmi \
     toplevel/himsg.cmi kernel/names.cmi contrib/correctness/past.cmi \
@@ -1880,6 +2059,16 @@ contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \
     lib/pp.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
     library/summary.cmx contrib/extraction/table.cmx kernel/term.cmx \
     pretyping/termops.cmx lib/util.cmx contrib/extraction/extraction.cmi 
+contrib/extraction/g_extraction.cmo: toplevel/cerrors.cmi \
+    parsing/egrammar.cmi contrib/extraction/extract_env.cmi \
+    parsing/genarg.cmi parsing/pcoq.cmi lib/pp.cmi \
+    contrib/extraction/table.cmi tactics/tacinterp.cmi \
+    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
+contrib/extraction/g_extraction.cmx: toplevel/cerrors.cmx \
+    parsing/egrammar.cmx contrib/extraction/extract_env.cmx \
+    parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
+    contrib/extraction/table.cmx tactics/tacinterp.cmx \
+    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx 
 contrib/extraction/haskell.cmo: contrib/extraction/miniml.cmi \
     contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \
     library/nametab.cmi contrib/extraction/ocaml.cmi lib/options.cmi \
@@ -1908,40 +2097,56 @@ contrib/extraction/ocaml.cmx: contrib/extraction/miniml.cmi \
     library/nametab.cmx lib/options.cmx lib/pp.cmx \
     contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
     contrib/extraction/ocaml.cmi 
-contrib/extraction/table.cmo: kernel/declarations.cmi library/global.cmi \
-    library/goptions.cmi library/lib.cmi library/libobject.cmi \
-    kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
-    library/summary.cmi kernel/term.cmi lib/util.cmi \
+contrib/extraction/table.cmo: kernel/declarations.cmi parsing/extend.cmi \
+    library/global.cmi library/goptions.cmi library/lib.cmi \
+    library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
+    parsing/printer.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
     toplevel/vernacinterp.cmi contrib/extraction/table.cmi 
-contrib/extraction/table.cmx: kernel/declarations.cmx library/global.cmx \
-    library/goptions.cmx library/lib.cmx library/libobject.cmx \
-    kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
-    library/summary.cmx kernel/term.cmx lib/util.cmx \
+contrib/extraction/table.cmx: kernel/declarations.cmx parsing/extend.cmx \
+    library/global.cmx library/goptions.cmx library/lib.cmx \
+    library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
+    parsing/printer.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx contrib/extraction/table.cmi 
-contrib/field/field.cmo: parsing/astterm.cmi parsing/coqast.cmi \
-    library/declare.cmi pretyping/evd.cmi library/global.cmi library/lib.cmi \
-    library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    proofs/proof_type.cmi contrib/ring/quote.cmo pretyping/reductionops.cmi \
-    contrib/ring/ring.cmo library/summary.cmi proofs/tacinterp.cmi \
-    proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
+contrib/field/field.cmo: parsing/astterm.cmi toplevel/cerrors.cmi \
+    parsing/coqast.cmi library/declare.cmi parsing/egrammar.cmi \
+    pretyping/evd.cmi parsing/extend.cmi parsing/genarg.cmi \
+    library/global.cmi library/lib.cmi library/libobject.cmi kernel/names.cmi \
+    library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
+    proofs/proof_type.cmi contrib/ring/quote.cmo pretyping/rawterm.cmi \
+    pretyping/reductionops.cmi proofs/refiner.cmi contrib/ring/ring.cmo \
+    library/summary.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi kernel/term.cmi \
+    pretyping/typing.cmi lib/util.cmi toplevel/vernacexpr.cmo \
     toplevel/vernacinterp.cmi 
-contrib/field/field.cmx: parsing/astterm.cmx parsing/coqast.cmx \
-    library/declare.cmx pretyping/evd.cmx library/global.cmx library/lib.cmx \
-    library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    proofs/proof_type.cmx contrib/ring/quote.cmx pretyping/reductionops.cmx \
-    contrib/ring/ring.cmx library/summary.cmx proofs/tacinterp.cmx \
-    proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
+contrib/field/field.cmx: parsing/astterm.cmx toplevel/cerrors.cmx \
+    parsing/coqast.cmx library/declare.cmx parsing/egrammar.cmx \
+    pretyping/evd.cmx parsing/extend.cmx parsing/genarg.cmx \
+    library/global.cmx library/lib.cmx library/libobject.cmx kernel/names.cmx \
+    library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
+    proofs/proof_type.cmx contrib/ring/quote.cmx pretyping/rawterm.cmx \
+    pretyping/reductionops.cmx proofs/refiner.cmx contrib/ring/ring.cmx \
+    library/summary.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx kernel/term.cmx \
+    pretyping/typing.cmx lib/util.cmx toplevel/vernacexpr.cmx \
     toplevel/vernacinterp.cmx 
 contrib/fourier/fourierR.cmo: parsing/astterm.cmi proofs/clenv.cmi \
-    tactics/equality.cmi pretyping/evd.cmi contrib/fourier/fourier.cmo \
-    library/global.cmi kernel/names.cmi parsing/pcoq.cmi \
-    contrib/ring/ring.cmo proofs/tacmach.cmi tactics/tactics.cmi \
-    kernel/term.cmi 
+    tactics/contradiction.cmi tactics/equality.cmi pretyping/evd.cmi \
+    contrib/fourier/fourier.cmo library/global.cmi kernel/names.cmi \
+    parsing/pcoq.cmi contrib/ring/ring.cmo proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+    toplevel/vernacexpr.cmo 
 contrib/fourier/fourierR.cmx: parsing/astterm.cmx proofs/clenv.cmx \
-    tactics/equality.cmx pretyping/evd.cmx contrib/fourier/fourier.cmx \
-    library/global.cmx kernel/names.cmx parsing/pcoq.cmx \
-    contrib/ring/ring.cmx proofs/tacmach.cmx tactics/tactics.cmx \
-    kernel/term.cmx 
+    tactics/contradiction.cmx tactics/equality.cmx pretyping/evd.cmx \
+    contrib/fourier/fourier.cmx library/global.cmx kernel/names.cmx \
+    parsing/pcoq.cmx contrib/ring/ring.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+    toplevel/vernacexpr.cmx 
+contrib/fourier/g_fourier.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
+    contrib/fourier/fourierR.cmo parsing/pcoq.cmi lib/pp.cmi \
+    parsing/pptactic.cmi proofs/refiner.cmi 
+contrib/fourier/g_fourier.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
+    contrib/fourier/fourierR.cmx parsing/pcoq.cmx lib/pp.cmx \
+    parsing/pptactic.cmx proofs/refiner.cmx 
 contrib/interface/blast.cmo: parsing/astterm.cmi tactics/auto.cmi \
     proofs/clenv.cmi toplevel/command.cmi contrib/interface/ctast.cmo \
     kernel/declarations.cmi library/declare.cmi tactics/eauto.cmo \
@@ -1950,11 +2155,11 @@ contrib/interface/blast.cmo: parsing/astterm.cmi tactics/auto.cmi \
     tactics/hipattern.cmi kernel/inductive.cmi proofs/logic.cmi \
     library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi \
     contrib/interface/pbp.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
-    parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
-    pretyping/rawterm.cmi kernel/reduction.cmi proofs/refiner.cmi \
-    kernel/sign.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
-    pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
+    parsing/pptactic.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+    proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
+    proofs/refiner.cmi kernel/sign.cmi proofs/tacmach.cmi \
+    pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
     toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \
     contrib/interface/blast.cmi 
 contrib/interface/blast.cmx: parsing/astterm.cmx tactics/auto.cmx \
@@ -1965,11 +2170,11 @@ contrib/interface/blast.cmx: parsing/astterm.cmx tactics/auto.cmx \
     tactics/hipattern.cmx kernel/inductive.cmx proofs/logic.cmx \
     library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx \
     contrib/interface/pbp.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
-    parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
-    pretyping/rawterm.cmx kernel/reduction.cmx proofs/refiner.cmx \
-    kernel/sign.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
-    pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
+    parsing/pptactic.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+    proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
+    proofs/refiner.cmx kernel/sign.cmx proofs/tacmach.cmx \
+    pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
     toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \
     contrib/interface/blast.cmi 
 contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
@@ -1977,69 +2182,77 @@ contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     pretyping/classops.cmi toplevel/command.cmi parsing/coqast.cmi \
     contrib/interface/ctast.cmo contrib/interface/dad.cmi \
     contrib/interface/debug_tac.cmi kernel/declarations.cmi \
-    library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
-    library/global.cmi contrib/interface/history.cmi library/lib.cmi \
-    library/libobject.cmi library/library.cmi \
-    toplevel/line_oriented_parser.cmi toplevel/mltop.cmi \
+    library/declare.cmi parsing/egrammar.cmi kernel/environ.cmi \
+    pretyping/evd.cmi parsing/genarg.cmi library/global.cmi \
+    contrib/interface/history.cmi library/lib.cmi library/libobject.cmi \
+    library/library.cmi toplevel/line_oriented_parser.cmi toplevel/mltop.cmi \
     contrib/interface/name_to_ast.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi contrib/interface/pbp.cmi proofs/pfedit.cmi \
-    lib/pp.cmi pretyping/pretyping.cmi parsing/printer.cmi \
+    library/nametab.cmi contrib/interface/pbp.cmi parsing/pcoq.cmi \
+    proofs/pfedit.cmi lib/pp.cmi parsing/pptactic.cmi pretyping/pretyping.cmi \
     proofs/proof_trees.cmi proofs/proof_type.cmi \
     toplevel/protectedtoplevel.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
-    parsing/search.cmi contrib/interface/showproof.cmi \
-    contrib/interface/showproof_ct.cmo proofs/tacinterp.cmi \
-    proofs/tacmach.cmi pretyping/tacred.cmi kernel/term.cmi \
+    proofs/refiner.cmi parsing/search.cmi contrib/interface/showproof.cmi \
+    contrib/interface/showproof_ct.cmo proofs/tacexpr.cmo \
+    tactics/tacinterp.cmi proofs/tacmach.cmi kernel/term.cmi \
     parsing/termast.cmi contrib/interface/translate.cmi lib/util.cmi \
-    toplevel/vernac.cmi toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \
-    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
+    toplevel/vernac.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi contrib/interface/vtp.cmi \
+    contrib/interface/xlate.cmi 
 contrib/interface/centaur.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \
     parsing/astterm.cmx contrib/interface/blast.cmx toplevel/cerrors.cmx \
     pretyping/classops.cmx toplevel/command.cmx parsing/coqast.cmx \
     contrib/interface/ctast.cmx contrib/interface/dad.cmx \
     contrib/interface/debug_tac.cmx kernel/declarations.cmx \
-    library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \
-    library/global.cmx contrib/interface/history.cmx library/lib.cmx \
-    library/libobject.cmx library/library.cmx \
-    toplevel/line_oriented_parser.cmx toplevel/mltop.cmx \
+    library/declare.cmx parsing/egrammar.cmx kernel/environ.cmx \
+    pretyping/evd.cmx parsing/genarg.cmx library/global.cmx \
+    contrib/interface/history.cmx library/lib.cmx library/libobject.cmx \
+    library/library.cmx toplevel/line_oriented_parser.cmx toplevel/mltop.cmx \
     contrib/interface/name_to_ast.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx contrib/interface/pbp.cmx proofs/pfedit.cmx \
-    lib/pp.cmx pretyping/pretyping.cmx parsing/printer.cmx \
+    library/nametab.cmx contrib/interface/pbp.cmx parsing/pcoq.cmx \
+    proofs/pfedit.cmx lib/pp.cmx parsing/pptactic.cmx pretyping/pretyping.cmx \
     proofs/proof_trees.cmx proofs/proof_type.cmx \
     toplevel/protectedtoplevel.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
-    parsing/search.cmx contrib/interface/showproof.cmx \
-    contrib/interface/showproof_ct.cmx proofs/tacinterp.cmx \
-    proofs/tacmach.cmx pretyping/tacred.cmx kernel/term.cmx \
+    proofs/refiner.cmx parsing/search.cmx contrib/interface/showproof.cmx \
+    contrib/interface/showproof_ct.cmx proofs/tacexpr.cmx \
+    tactics/tacinterp.cmx proofs/tacmach.cmx kernel/term.cmx \
     parsing/termast.cmx contrib/interface/translate.cmx lib/util.cmx \
-    toplevel/vernac.cmx toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \
-    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
+    toplevel/vernac.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx contrib/interface/vtp.cmx \
+    contrib/interface/xlate.cmx 
 contrib/interface/ctast.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \
     kernel/names.cmi 
 contrib/interface/ctast.cmx: parsing/ast.cmx parsing/coqast.cmx lib/dyn.cmx \
     kernel/names.cmx 
-contrib/interface/dad.cmo: parsing/astterm.cmi contrib/interface/ctast.cmo \
-    kernel/environ.cmi pretyping/evd.cmi library/global.cmi kernel/names.cmi \
+contrib/interface/dad.cmo: parsing/astterm.cmi parsing/coqast.cmi \
+    contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evd.cmi \
+    parsing/genarg.cmi library/global.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/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
-    parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi contrib/interface/dad.cmi 
-contrib/interface/dad.cmx: parsing/astterm.cmx contrib/interface/ctast.cmx \
-    kernel/environ.cmx pretyping/evd.cmx library/global.cmx kernel/names.cmx \
+    pretyping/rawterm.cmi kernel/reduction.cmi proofs/tacexpr.cmo \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \
+    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi \
+    contrib/interface/dad.cmi 
+contrib/interface/dad.cmx: parsing/astterm.cmx parsing/coqast.cmx \
+    contrib/interface/ctast.cmx kernel/environ.cmx pretyping/evd.cmx \
+    parsing/genarg.cmx library/global.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/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
-    parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx contrib/interface/dad.cmi 
+    pretyping/rawterm.cmx kernel/reduction.cmx proofs/tacexpr.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx parsing/termast.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 lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
-    lib/util.cmi contrib/interface/debug_tac.cmi 
+    parsing/coqast.cmi parsing/genarg.cmi lib/pp.cmi parsing/pptactic.cmi \
+    proofs/proof_trees.cmi proofs/proof_type.cmi proofs/refiner.cmi \
+    proofs/tacexpr.cmo tactics/tacinterp.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi lib/util.cmi contrib/interface/debug_tac.cmi 
 contrib/interface/debug_tac.cmx: parsing/ast.cmx toplevel/cerrors.cmx \
-    parsing/coqast.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
-    lib/util.cmx contrib/interface/debug_tac.cmi 
+    parsing/coqast.cmx parsing/genarg.cmx lib/pp.cmx parsing/pptactic.cmx \
+    proofs/proof_trees.cmx proofs/proof_type.cmx proofs/refiner.cmx \
+    proofs/tacexpr.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx lib/util.cmx contrib/interface/debug_tac.cmi 
 contrib/interface/history.cmo: contrib/interface/paths.cmi \
     contrib/interface/history.cmi 
 contrib/interface/history.cmx: contrib/interface/paths.cmx \
@@ -2053,7 +2266,7 @@ contrib/interface/name_to_ast.cmo: parsing/ast.cmi pretyping/classops.cmi \
     library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
     parsing/prettyp.cmi kernel/reduction.cmi kernel/sign.cmi \
     pretyping/syntax_def.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \
-    contrib/interface/name_to_ast.cmi 
+    toplevel/vernacexpr.cmo contrib/interface/name_to_ast.cmi 
 contrib/interface/name_to_ast.cmx: parsing/ast.cmx pretyping/classops.cmx \
     parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \
     kernel/environ.cmx library/global.cmx library/impargs.cmx \
@@ -2061,40 +2274,42 @@ contrib/interface/name_to_ast.cmx: parsing/ast.cmx pretyping/classops.cmx \
     library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
     parsing/prettyp.cmx kernel/reduction.cmx kernel/sign.cmx \
     pretyping/syntax_def.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \
-    contrib/interface/name_to_ast.cmi 
+    toplevel/vernacexpr.cmx contrib/interface/name_to_ast.cmi 
 contrib/interface/parse.cmo: contrib/interface/ascent.cmi \
     toplevel/cerrors.cmi config/coq_config.cmi contrib/interface/ctast.cmo \
     parsing/esyntax.cmi library/libobject.cmi library/library.cmi \
-    contrib/interface/line_parser.cmi toplevel/metasyntax.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi \
-    lib/pp.cmi lib/system.cmi lib/util.cmi contrib/interface/vtp.cmi \
-    contrib/interface/xlate.cmi 
+    contrib/interface/line_parser.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi lib/system.cmi \
+    lib/util.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
+    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
 contrib/interface/parse.cmx: contrib/interface/ascent.cmi \
     toplevel/cerrors.cmx config/coq_config.cmx contrib/interface/ctast.cmx \
     parsing/esyntax.cmx library/libobject.cmx library/library.cmx \
-    contrib/interface/line_parser.cmx toplevel/metasyntax.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx \
-    lib/pp.cmx lib/system.cmx lib/util.cmx contrib/interface/vtp.cmx \
-    contrib/interface/xlate.cmx 
+    contrib/interface/line_parser.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx lib/system.cmx \
+    lib/util.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
+    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/paths.cmo: contrib/interface/paths.cmi 
 contrib/interface/paths.cmx: contrib/interface/paths.cmi 
-contrib/interface/pbp.cmo: parsing/astterm.cmi parsing/coqlib.cmi \
-    contrib/interface/ctast.cmo library/declare.cmi kernel/environ.cmi \
-    pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \
-    proofs/logic.cmi kernel/names.cmi library/nametab.cmi \
-    pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/pretyping.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
-    kernel/reduction.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+contrib/interface/pbp.cmo: parsing/astterm.cmi parsing/coqast.cmi \
+    parsing/coqlib.cmi contrib/interface/ctast.cmo library/declare.cmi \
+    kernel/environ.cmi pretyping/evd.cmi library/global.cmi \
+    tactics/hipattern.cmi proofs/logic.cmi kernel/names.cmi \
+    library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
+    pretyping/pretyping.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+    pretyping/rawterm.cmi kernel/reduction.cmi proofs/tacexpr.cmo \
+    tactics/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi parsing/termast.cmi \
     pretyping/typing.cmi lib/util.cmi contrib/interface/pbp.cmi 
-contrib/interface/pbp.cmx: parsing/astterm.cmx parsing/coqlib.cmx \
-    contrib/interface/ctast.cmx library/declare.cmx kernel/environ.cmx \
-    pretyping/evd.cmx library/global.cmx tactics/hipattern.cmx \
-    proofs/logic.cmx kernel/names.cmx library/nametab.cmx \
-    pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx pretyping/pretyping.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
-    kernel/reduction.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+contrib/interface/pbp.cmx: parsing/astterm.cmx parsing/coqast.cmx \
+    parsing/coqlib.cmx contrib/interface/ctast.cmx library/declare.cmx \
+    kernel/environ.cmx pretyping/evd.cmx library/global.cmx \
+    tactics/hipattern.cmx proofs/logic.cmx kernel/names.cmx \
+    library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \
+    pretyping/pretyping.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
+    pretyping/rawterm.cmx kernel/reduction.cmx proofs/tacexpr.cmx \
+    tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \
     pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi 
 contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
     parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
@@ -2106,24 +2321,28 @@ contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
     contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \
     proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \
-    kernel/environ.cmi pretyping/evd.cmi library/global.cmi \
-    kernel/inductive.cmi pretyping/inductiveops.cmi library/nameops.cmi \
-    kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
-    contrib/interface/showproof_ct.cmo kernel/sign.cmi proofs/tacmach.cmi \
-    kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \
-    contrib/interface/translate.cmi pretyping/typing.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi contrib/interface/showproof.cmi 
+    kernel/environ.cmi pretyping/evd.cmi parsing/genarg.cmi \
+    library/global.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \
+    library/nameops.cmi kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi \
+    parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+    pretyping/rawterm.cmi pretyping/reductionops.cmi \
+    contrib/interface/showproof_ct.cmo kernel/sign.cmi proofs/tacexpr.cmo \
+    proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \
+    pretyping/termops.cmi contrib/interface/translate.cmi \
+    pretyping/typing.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+    contrib/interface/showproof.cmi 
 contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \
     proofs/clenv.cmx parsing/coqast.cmx kernel/declarations.cmx \
-    kernel/environ.cmx pretyping/evd.cmx library/global.cmx \
-    kernel/inductive.cmx pretyping/inductiveops.cmx library/nameops.cmx \
-    kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \
-    contrib/interface/showproof_ct.cmx kernel/sign.cmx proofs/tacmach.cmx \
-    kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \
-    contrib/interface/translate.cmx pretyping/typing.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx contrib/interface/showproof.cmi 
+    kernel/environ.cmx pretyping/evd.cmx parsing/genarg.cmx \
+    library/global.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \
+    library/nameops.cmx kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx \
+    parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
+    pretyping/rawterm.cmx pretyping/reductionops.cmx \
+    contrib/interface/showproof_ct.cmx kernel/sign.cmx proofs/tacexpr.cmx \
+    proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \
+    pretyping/termops.cmx contrib/interface/translate.cmx \
+    pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+    contrib/interface/showproof.cmi 
 contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \
     pretyping/evd.cmi library/libobject.cmi library/library.cmi \
@@ -2143,11 +2362,17 @@ contrib/interface/vtp.cmo: contrib/interface/ascent.cmi \
 contrib/interface/vtp.cmx: contrib/interface/ascent.cmi \
     contrib/interface/vtp.cmi 
 contrib/interface/xlate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
-    contrib/interface/ctast.cmo library/nameops.cmi kernel/names.cmi \
-    lib/util.cmi contrib/interface/xlate.cmi 
+    parsing/astterm.cmi parsing/coqast.cmi contrib/interface/ctast.cmo \
+    tactics/extraargs.cmi parsing/genarg.cmi library/nameops.cmi \
+    kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \
+    proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo \
+    contrib/interface/xlate.cmi 
 contrib/interface/xlate.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \
-    contrib/interface/ctast.cmx library/nameops.cmx kernel/names.cmx \
-    lib/util.cmx contrib/interface/xlate.cmi 
+    parsing/astterm.cmx parsing/coqast.cmx contrib/interface/ctast.cmx \
+    tactics/extraargs.cmx parsing/genarg.cmx library/nameops.cmx \
+    kernel/names.cmx library/nametab.cmx pretyping/rawterm.cmx \
+    proofs/tacexpr.cmx lib/util.cmx toplevel/vernacexpr.cmx \
+    contrib/interface/xlate.cmi 
 contrib/jprover/jall.cmo: contrib/jprover/jlogic.cmi \
     contrib/jprover/jterm.cmi contrib/jprover/jtunify.cmi \
     contrib/jprover/opname.cmi contrib/jprover/jall.cmi 
@@ -2158,20 +2383,24 @@ contrib/jprover/jlogic.cmo: contrib/jprover/jterm.cmi \
     contrib/jprover/opname.cmi contrib/jprover/jlogic.cmi 
 contrib/jprover/jlogic.cmx: contrib/jprover/jterm.cmx \
     contrib/jprover/opname.cmx contrib/jprover/jlogic.cmi 
-contrib/jprover/jprover.cmo: proofs/clenv.cmi library/global.cmi \
-    tactics/hipattern.cmi contrib/jprover/jall.cmi contrib/jprover/jlogic.cmi \
-    contrib/jprover/jterm.cmi kernel/names.cmi pretyping/pattern.cmi \
-    lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi kernel/reduction.cmi \
-    pretyping/reductionops.cmi tactics/tacentries.cmi proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
-    pretyping/termops.cmi lib/util.cmi 
-contrib/jprover/jprover.cmx: proofs/clenv.cmx library/global.cmx \
-    tactics/hipattern.cmx contrib/jprover/jall.cmx contrib/jprover/jlogic.cmx \
-    contrib/jprover/jterm.cmx kernel/names.cmx pretyping/pattern.cmx \
-    lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \
-    pretyping/reductionops.cmx tactics/tacentries.cmx proofs/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
-    pretyping/termops.cmx lib/util.cmx 
+contrib/jprover/jprover.cmo: toplevel/cerrors.cmi proofs/clenv.cmi \
+    parsing/egrammar.cmi parsing/genarg.cmi library/global.cmi \
+    tactics/hiddentac.cmi tactics/hipattern.cmi contrib/jprover/jall.cmi \
+    contrib/jprover/jlogic.cmi contrib/jprover/jterm.cmi kernel/names.cmi \
+    pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
+    parsing/printer.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
+    kernel/reduction.cmi pretyping/reductionops.cmi proofs/refiner.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi pretyping/termops.cmi lib/util.cmi 
+contrib/jprover/jprover.cmx: toplevel/cerrors.cmx proofs/clenv.cmx \
+    parsing/egrammar.cmx parsing/genarg.cmx library/global.cmx \
+    tactics/hiddentac.cmx tactics/hipattern.cmx contrib/jprover/jall.cmx \
+    contrib/jprover/jlogic.cmx contrib/jprover/jterm.cmx kernel/names.cmx \
+    pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
+    parsing/printer.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
+    kernel/reduction.cmx pretyping/reductionops.cmx proofs/refiner.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx pretyping/termops.cmx lib/util.cmx 
 contrib/jprover/jterm.cmo: contrib/jprover/opname.cmi \
     contrib/jprover/jterm.cmi 
 contrib/jprover/jterm.cmx: contrib/jprover/opname.cmx \
@@ -2181,34 +2410,56 @@ contrib/jprover/jtunify.cmx: contrib/jprover/jtunify.cmi
 contrib/jprover/opname.cmo: contrib/jprover/opname.cmi 
 contrib/jprover/opname.cmx: contrib/jprover/opname.cmi 
 contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \
-    kernel/closure.cmi parsing/coqlib.cmi kernel/declarations.cmi \
-    library/declare.cmi kernel/environ.cmi tactics/equality.cmi \
-    proofs/evar_refiner.cmi library/global.cmi kernel/inductive.cmi \
-    proofs/logic.cmi library/nameops.cmi kernel/names.cmi library/nametab.cmi \
+    kernel/closure.cmi tactics/contradiction.cmi parsing/coqlib.cmi \
+    kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
+    tactics/equality.cmi proofs/evar_refiner.cmi library/global.cmi \
+    library/goptions.cmi kernel/inductive.cmi proofs/logic.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi \
     contrib/omega/omega.cmo lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi tactics/tactics.cmi kernel/term.cmi \
-    pretyping/termops.cmi lib/util.cmi 
+    proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi 
 contrib/omega/coq_omega.cmx: parsing/ast.cmx proofs/clenv.cmx \
-    kernel/closure.cmx parsing/coqlib.cmx kernel/declarations.cmx \
-    library/declare.cmx kernel/environ.cmx tactics/equality.cmx \
-    proofs/evar_refiner.cmx library/global.cmx kernel/inductive.cmx \
-    proofs/logic.cmx library/nameops.cmx kernel/names.cmx library/nametab.cmx \
+    kernel/closure.cmx tactics/contradiction.cmx parsing/coqlib.cmx \
+    kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
+    tactics/equality.cmx proofs/evar_refiner.cmx library/global.cmx \
+    library/goptions.cmx kernel/inductive.cmx proofs/logic.cmx \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx \
     contrib/omega/omega.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx tactics/tactics.cmx kernel/term.cmx \
-    pretyping/termops.cmx lib/util.cmx 
+    proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
+    kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx 
+contrib/omega/g_omega.cmo: toplevel/cerrors.cmi contrib/omega/coq_omega.cmo \
+    parsing/egrammar.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
+    proofs/refiner.cmi 
+contrib/omega/g_omega.cmx: toplevel/cerrors.cmx contrib/omega/coq_omega.cmx \
+    parsing/egrammar.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
+    proofs/refiner.cmx 
 contrib/omega/omega.cmo: lib/util.cmi 
 contrib/omega/omega.cmx: lib/util.cmx 
+contrib/ring/g_quote.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
+    parsing/genarg.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
+    contrib/ring/quote.cmo proofs/refiner.cmi 
+contrib/ring/g_quote.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
+    parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
+    contrib/ring/quote.cmx proofs/refiner.cmx 
+contrib/ring/g_ring.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
+    parsing/genarg.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
+    contrib/ring/quote.cmo proofs/refiner.cmi contrib/ring/ring.cmo \
+    toplevel/vernacinterp.cmi 
+contrib/ring/g_ring.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
+    parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
+    contrib/ring/quote.cmx proofs/refiner.cmx contrib/ring/ring.cmx \
+    toplevel/vernacinterp.cmx 
 contrib/ring/quote.cmo: library/declare.cmi kernel/environ.cmi \
     library/global.cmi pretyping/instantiate.cmi kernel/names.cmi \
     library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi proofs/tacmach.cmi \
+    proofs/proof_trees.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
     tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi 
 contrib/ring/quote.cmx: library/declare.cmx kernel/environ.cmx \
     library/global.cmx pretyping/instantiate.cmx kernel/names.cmx \
     library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx proofs/tacmach.cmx \
+    proofs/proof_trees.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \
     tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx 
 contrib/ring/ring.cmo: parsing/astterm.cmi kernel/closure.cmi \
     parsing/coqlib.cmi library/declare.cmi tactics/equality.cmi \
@@ -2216,28 +2467,34 @@ contrib/ring/ring.cmo: parsing/astterm.cmi kernel/closure.cmi \
     tactics/hipattern.cmi library/lib.cmi library/libobject.cmi \
     library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
     pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi contrib/ring/quote.cmo \
-    pretyping/reductionops.cmi tactics/setoid_replace.cmi library/summary.cmi \
-    proofs/tacmach.cmi pretyping/tacred.cmi tactics/tactics.cmi \
-    kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi 
+    proofs/proof_trees.cmi contrib/ring/quote.cmo pretyping/reductionops.cmi \
+    tactics/setoid_replace.cmi library/summary.cmi proofs/tacexpr.cmo \
+    proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
+    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
 contrib/ring/ring.cmx: parsing/astterm.cmx kernel/closure.cmx \
     parsing/coqlib.cmx library/declare.cmx tactics/equality.cmx \
     pretyping/evd.cmx library/global.cmx tactics/hiddentac.cmx \
     tactics/hipattern.cmx library/lib.cmx library/libobject.cmx \
     library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
     pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx contrib/ring/quote.cmx \
-    pretyping/reductionops.cmx tactics/setoid_replace.cmx library/summary.cmx \
-    proofs/tacmach.cmx pretyping/tacred.cmx tactics/tactics.cmx \
-    kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx 
+    proofs/proof_trees.cmx contrib/ring/quote.cmx pretyping/reductionops.cmx \
+    tactics/setoid_replace.cmx library/summary.cmx proofs/tacexpr.cmx \
+    proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
+    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx 
 contrib/romega/const_omega.cmo: library/declare.cmi library/global.cmi \
     kernel/names.cmi library/nametab.cmi kernel/term.cmi \
     pretyping/termops.cmi lib/util.cmi 
 contrib/romega/const_omega.cmx: library/declare.cmx library/global.cmx \
     kernel/names.cmx library/nametab.cmx kernel/term.cmx \
     pretyping/termops.cmx lib/util.cmx 
+contrib/romega/g_romega.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
+    parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi proofs/refiner.cmi \
+    contrib/romega/refl_omega.cmo 
+contrib/romega/g_romega.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
+    parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx proofs/refiner.cmx \
+    contrib/romega/refl_omega.cmx 
 contrib/romega/refl_omega.cmo: parsing/ast.cmi tactics/auto.cmi \
     proofs/clenv.cmi contrib/romega/const_omega.cmo \
     contrib/omega/coq_omega.cmo kernel/environ.cmi kernel/inductive.cmi \
@@ -2268,20 +2525,54 @@ contrib/xml/xmlcommand.cmx: kernel/declarations.cmx library/declare.cmx \
     kernel/safe_typing.cmx kernel/sign.cmx lib/system.cmx proofs/tacmach.cmx \
     kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx \
     contrib/xml/xmlcommand.cmi 
-contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \
-    contrib/xml/xmlcommand.cmi 
-contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \
-    contrib/xml/xmlcommand.cmx 
+contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
+    parsing/extend.cmi parsing/genarg.cmi parsing/pcoq.cmi lib/pp.cmi \
+    parsing/pptactic.cmi tactics/tacinterp.cmi lib/util.cmi \
+    toplevel/vernacinterp.cmi contrib/xml/xmlcommand.cmi 
+contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
+    parsing/extend.cmx parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
+    parsing/pptactic.cmx tactics/tacinterp.cmx lib/util.cmx \
+    toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx 
 contrib/xml/xml.cmo: contrib/xml/xml.cmi 
 contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 tactics/tauto.cmx: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
+tactics/eqdecide.cmo: parsing/grammar.cma
+tactics/eqdecide.cmx: parsing/grammar.cma
+tactics/extraargs.cmo: parsing/grammar.cma
+tactics/extraargs.cmx: parsing/grammar.cma
+tactics/extratactics.cmo: parsing/grammar.cma
+tactics/extratactics.cmx: parsing/grammar.cma
+tactics/eauto.cmo: parsing/grammar.cma
+tactics/eauto.cmx: parsing/grammar.cma
+contrib/interface/debug_tac.cmo: parsing/grammar.cma
+contrib/interface/debug_tac.cmx: parsing/grammar.cma
+contrib/interface/centaur.cmo: parsing/grammar.cma
+contrib/interface/centaur.cmx: parsing/grammar.cma
 contrib/correctness/psyntax.cmo: parsing/grammar.cma
 contrib/correctness/psyntax.cmx: parsing/grammar.cma
+contrib/omega/g_omega.cmo: parsing/grammar.cma
+contrib/omega/g_omega.cmx: parsing/grammar.cma
+contrib/romega/g_romega.cmo: parsing/grammar.cma
+contrib/romega/g_romega.cmx: parsing/grammar.cma
+contrib/ring/g_quote.cmo: parsing/grammar.cma
+contrib/ring/g_quote.cmx: parsing/grammar.cma
+contrib/ring/g_ring.cmo: parsing/grammar.cma
+contrib/ring/g_ring.cmx: parsing/grammar.cma
 contrib/field/field.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 contrib/field/field.cmx: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
+contrib/fourier/g_fourier.cmo: parsing/grammar.cma
+contrib/fourier/g_fourier.cmx: parsing/grammar.cma
+contrib/extraction/g_extraction.cmo: parsing/grammar.cma
+contrib/extraction/g_extraction.cmx: parsing/grammar.cma
+contrib/xml/xmlentries.cmo: parsing/grammar.cma
+contrib/xml/xmlentries.cmx: parsing/grammar.cma
+contrib/jprover/jprover.cmo: parsing/grammar.cma
+contrib/jprover/jprover.cmx: parsing/grammar.cma
 parsing/lexer.cmo: 
 parsing/lexer.cmx: 
+parsing/q_util.cmo: 
+parsing/q_util.cmx: 
 parsing/q_coqast.cmo: 
 parsing/q_coqast.cmx: 
 parsing/g_prim.cmo: 
@@ -2304,8 +2595,10 @@ parsing/g_tactic.cmo: parsing/grammar.cma
 parsing/g_tactic.cmx: parsing/grammar.cma
 parsing/g_ltac.cmo: parsing/grammar.cma
 parsing/g_ltac.cmx: parsing/grammar.cma
-parsing/extend.cmo: parsing/grammar.cma
-parsing/extend.cmx: parsing/grammar.cma
+parsing/tacextend.cmo: 
+parsing/tacextend.cmx: 
+parsing/vernacextend.cmo: 
+parsing/vernacextend.cmx: 
 toplevel/mltop.cmo: 
 toplevel/mltop.cmx: 
 lib/pp.cmo: 
diff --git a/.depend.camlp4 b/.depend.camlp4
index 94a85c9807..bbbdb186cd 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -1,7 +1,22 @@
 tactics/tauto.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
+tactics/eqdecide.ml: parsing/grammar.cma
+tactics/extraargs.ml: parsing/grammar.cma
+tactics/extratactics.ml: parsing/grammar.cma
+tactics/eauto.ml: parsing/grammar.cma
+contrib/interface/debug_tac.ml: parsing/grammar.cma
+contrib/interface/centaur.ml: parsing/grammar.cma
 contrib/correctness/psyntax.ml: parsing/grammar.cma
+contrib/omega/g_omega.ml: parsing/grammar.cma
+contrib/romega/g_romega.ml: parsing/grammar.cma
+contrib/ring/g_quote.ml: parsing/grammar.cma
+contrib/ring/g_ring.ml: parsing/grammar.cma
 contrib/field/field.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
+contrib/fourier/g_fourier.ml: parsing/grammar.cma
+contrib/extraction/g_extraction.ml: parsing/grammar.cma
+contrib/xml/xmlentries.ml: parsing/grammar.cma
+contrib/jprover/jprover.ml: parsing/grammar.cma
 parsing/lexer.ml: 
+parsing/q_util.ml: 
 parsing/q_coqast.ml: 
 parsing/g_prim.ml: 
 parsing/pcoq.ml: 
@@ -13,7 +28,8 @@ parsing/g_cases.ml: parsing/grammar.cma
 parsing/g_constr.ml: parsing/grammar.cma
 parsing/g_tactic.ml: parsing/grammar.cma
 parsing/g_ltac.ml: parsing/grammar.cma
-parsing/extend.ml: parsing/grammar.cma
+parsing/tacextend.ml: 
+parsing/vernacextend.ml: 
 toplevel/mltop.ml: 
 lib/pp.ml: 
 contrib/xml/xml.ml: 
diff --git a/.depend.coq b/.depend.coq
index 928dd10deb..df11634755 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -1,8 +1,6 @@
-contrib/extraction/Extraction.vo: contrib/extraction/Extraction.v
-contrib/jprover/JProver.vo: contrib/jprover/JProver.v
+contrib/interface/Centaur.vo: contrib/interface/Centaur.v
 contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/fourier/Fourier_util.vo contrib/field/Field.vo theories/Reals/DiscrR.vo
 contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo
-contrib/interface/Centaur.vo: contrib/interface/Centaur.v
 contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v
 contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
 contrib/correctness/ProgWf.vo: contrib/correctness/ProgWf.v theories/ZArith/ZArith.vo theories/Arith/Wf_nat.vo
@@ -12,7 +10,6 @@ contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/co
 contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo
 contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo contrib/correctness/ProgWf.vo contrib/correctness/Arrays.vo
 contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v contrib/correctness/ProgInt.vo
-contrib/xml/Xml.vo: contrib/xml/Xml.v
 contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo
 contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v contrib/ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo
 contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Arith/Peano_dec.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo
@@ -29,8 +26,7 @@ contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_
 contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
 contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/omega/Omega.vo contrib/romega/ReflOmegaCore.vo
 contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/PolyList.vo theories/Bool/Bool.vo theories/ZArith/ZArith.vo
-contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
-contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith.vo theories/Arith/Minus.vo contrib/omega/OmegaSyntax.vo
+contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith.vo theories/Arith/Minus.vo
 theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
 theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/PolyList.vo theories/Sets/Multiset.vo
 theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo
@@ -136,7 +132,7 @@ theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo
 theories/Bool/Bool.vo: theories/Bool/Bool.v
 theories/Arith/Max.vo: theories/Arith/Max.v theories/Arith/Arith.vo
 theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo
-theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo
+theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/ArithSyntax.vo
 theories/Arith/Euclid.vo: theories/Arith/Euclid.v theories/Arith/Mult.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
 theories/Arith/Peano_dec.vo: theories/Arith/Peano_dec.v theories/Logic/Decidable.vo
 theories/Arith/EqNat.vo: theories/Arith/EqNat.v
@@ -152,6 +148,7 @@ theories/Arith/Le.vo: theories/Arith/Le.v
 theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo
 theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
+theories/Arith/ArithSyntax.vo: theories/Arith/ArithSyntax.v
 theories/Logic/JMeq.vo: theories/Logic/JMeq.v
 theories/Logic/Decidable.vo: theories/Logic/Decidable.v
 theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v
diff --git a/CHANGES b/CHANGES
index f9ba8efbed..81d1a59e23 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,39 @@
+Changes from V7.3 to ????
+-------------------------
+
+Language
+
+- Inductive definitions now accept ">" in constructor types to declare
+  the corresponding constructor as a coercion.
+
+ML tactic and vernacular commands
+
+- "Grammar tactic" and "Grammar vernac" of type "ast" are no longer
+  supported (only "Grammar tactic simple_tactic" of type "tactic"
+  remains available).
+- Concrete syntax for ML written vernacular commands and tactics is
+  now declared at ML level using camlp4 macros TACTIC EXTEND et VERNAC
+  COMMAND EXTEND.
+
+Tactic definitions
+
+- static globalisation of identifiers and global references (source of
+  incompatibilities, especially, Recursive keyword is required for
+  mutually recursive definitions).
+
+Tactics
+
+- Double Induction now referring to hypotheses like "Intro until"
+- "Inversion" now applies also on quantified hypotheses (naming as
+  for Intros until)
+- NewDestruct now accepts terms with missing hypotheses
+
+Miscellaneous
+
+- Printing Coercion now used through the standard keywords Set/Add, Test, Print
+
 Changes from V7.2 to V7.3
-=========================
+-------------------------
 
 Language
 
diff --git a/Makefile b/Makefile
index b933ce3cc9..3282b3f915 100644
--- a/Makefile
+++ b/Makefile
@@ -54,7 +54,7 @@ DEPFLAGS=$(LOCALINCLUDES)
 
 OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS)
 OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS)
-CAMLP4EXTENDFLAGS=-I . pa_extend.cmo q_MLast.cmo
+CAMLP4EXTENDFLAGS=-I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo
 CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p'
 
 COQINCLUDES=          # coqtop includes itself the needed paths
@@ -101,45 +101,62 @@ PRETYPING=pretyping/termops.cmo \
           pretyping/coercion.cmo pretyping/cases.cmo pretyping/pretyping.cmo \
 	  pretyping/syntax_def.cmo pretyping/pattern.cmo 
 
-PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
-	parsing/termast.cmo parsing/astterm.cmo parsing/coqlib.cmo \
-	parsing/g_prim.cmo parsing/g_basevernac.cmo \
+PARSING=parsing/lexer.cmo parsing/coqast.cmo \
+        parsing/genarg.cmo proofs/tacexpr.cmo parsing/ast.cmo \
+        parsing/termast.cmo parsing/astterm.cmo \
+	parsing/extend.cmo parsing/esyntax.cmo \
+        parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo \
+	parsing/coqlib.cmo parsing/prettyp.cmo parsing/search.cmo
+
+HIGHPARSING= parsing/g_prim.cmo parsing/g_basevernac.cmo \
 	parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \
 	parsing/g_ltac.cmo parsing/g_constr.cmo parsing/g_cases.cmo \
-        parsing/extend.cmo parsing/esyntax.cmo \
-	parsing/printer.cmo parsing/prettyp.cmo parsing/search.cmo \
-        parsing/egrammar.cmo \
-        parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo
+	parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo
 
 ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo
 
 PROOFS=proofs/proof_type.cmo proofs/proof_trees.cmo proofs/logic.cmo \
        proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \
        proofs/clenv.cmo proofs/pfedit.cmo \
-       proofs/tactic_debug.cmo proofs/tacinterp.cmo
+       proofs/tactic_debug.cmo
 
 TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
         tactics/nbtermdn.cmo tactics/hipattern.cmo tactics/wcclausenv.cmo \
-        tactics/tacticals.cmo tactics/tactics.cmo tactics/tacentries.cmo \
-        tactics/hiddentac.cmo tactics/elim.cmo
-
-TOPLEVEL=toplevel/himsg.cmo toplevel/cerrors.cmo \
-         toplevel/metasyntax.cmo toplevel/command.cmo toplevel/class.cmo \
-         toplevel/record.cmo toplevel/recordobj.cmo \
-         toplevel/discharge.cmo toplevel/vernacinterp.cmo toplevel/mltop.cmo \
-         toplevel/vernac.cmo toplevel/vernacentries.cmo \
+        tactics/tacticals.cmo tactics/tactics.cmo \
+        tactics/hiddentac.cmo tactics/elim.cmo \
+	tactics/dhyp.cmo tactics/auto.cmo tactics/tacinterp.cmo
+
+TOPLEVEL=toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \
+	 toplevel/command.cmo toplevel/record.cmo toplevel/recordobj.cmo \
+         toplevel/discharge.cmo toplevel/vernacexpr.cmo \
+         toplevel/vernacinterp.cmo toplevel/mltop.cmo \
+         parsing/pcoq.cmo parsing/egrammar.cmo toplevel/metasyntax.cmo \
+         toplevel/vernacentries.cmo toplevel/vernac.cmo \
 	 toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \
          toplevel/toplevel.cmo toplevel/usage.cmo \
 	 toplevel/coqinit.cmo toplevel/coqtop.cmo
 
-HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/setoid_replace.cmo\
-	    tactics/equality.cmo \
-            tactics/inv.cmo tactics/leminv.cmo tactics/eauto.cmo \
-            tactics/autorewrite.cmo tactics/refine.cmo tactics/eqdecide.cmo
+HIGHTACTICS=tactics/setoid_replace.cmo tactics/equality.cmo \
+            tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \
+            tactics/autorewrite.cmo tactics/refine.cmo \
+	    tactics/extraargs.cmo tactics/extratactics.cmo tactics/eauto.cmo
+
+QUOTIFY=parsing/qast.cmo parsing/q_prim.cmo parsing/q_tactic.cmo
+
+parsing/q_prim.ml4: parsing/g_prim.ml4
+	camlp4o -I parsing grammar.cma pa_ifdef.cmo pa_extend.cmo pr_o.cmo pr_extend.cmo -quotify -DQuotify -o parsing/q_prim.ml4 -impl parsing/g_prim.ml4
+
+parsing/q_tactic.ml4: parsing/g_tactic.ml4
+	camlp4o -I parsing grammar.cma pa_ifdef.cmo pa_extend.cmo pr_o.cmo pr_extend.cmo -quotify -DQuotify -o parsing/q_tactic.ml4 -impl parsing/g_tactic.ml4
 
-SPECTAC=tactics/tauto.ml4
+parsing/q_ltac.ml4: parsing/g_ltac.ml4
+	camlp4o -I parsing grammar.cma pa_ifdef.cmo pa_extend.cmo pr_o.cmo pr_extend.cmo -quotify -DQuotify -o parsing/q_ltac.ml4 -impl parsing/g_ltac.ml4
+
+SPECTAC= tactics/tauto.ml4 tactics/eqdecide.ml4
 USERTAC = $(SPECTAC)
-ML4FILES += $(USERTAC)
+ML4FILES += $(USERTAC) tactics/extraargs.ml4 tactics/extratactics.ml4 \
+	tactics/eauto.ml4 
+
 USERTACCMO=$(USERTAC:.ml4=.cmo)
 USERTACCMX=$(USERTAC:.ml4=.cmx)
 
@@ -153,11 +170,13 @@ INTERFACE=contrib/interface/vtp.cmo \
 	contrib/interface/showproof_ct.cmo contrib/interface/showproof.cmo \
 	contrib/interface/blast.cmo contrib/interface/centaur.cmo
 
+ML4FILES += contrib/interface/debug_tac.ml4 contrib/interface/centaur.ml4
+
 PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \
 	lib/util.cmo lib/dyn.cmo lib/gmap.cmo lib/gmapl.cmo \
         lib/predicate.cmo lib/hashcons.cmo lib/profile.cmo \
         lib/system.cmo lib/bstack.cmo lib/edit.cmo lib/options.cmo \
-	lib/rtree.cmo \
+	lib/rtree.cmo lib/gset.cmo lib/tlm.cmo \
         kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo \
         kernel/term.cmo kernel/sign.cmo kernel/declarations.cmo \
 	kernel/environ.cmo \
@@ -167,6 +186,7 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \
 	library/nameops.cmo library/libobject.cmo library/summary.cmo \
 	library/nametab.cmo library/lib.cmo library/global.cmo \
 	library/library.cmo lib/options.cmo library/impargs.cmo \
+        library/goptions.cmo \
 	pretyping/evd.cmo pretyping/instantiate.cmo \
         pretyping/termops.cmo \
         pretyping/reductionops.cmo pretyping/retyping.cmo library/declare.cmo \
@@ -177,35 +197,53 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \
 	pretyping/coercion.cmo pretyping/inductiveops.cmo pretyping/cases.cmo \
         pretyping/indrec.cmo \
 	pretyping/pretyping.cmo pretyping/syntax_def.cmo \
-	parsing/lexer.cmo parsing/coqast.cmo \
+	parsing/lexer.cmo parsing/coqast.cmo parsing/genarg.cmo \
+	proofs/tacexpr.cmo toplevel/vernacexpr.cmo \
 	parsing/pcoq.cmo parsing/ast.cmo \
 	parsing/g_prim.cmo parsing/g_basevernac.cmo \
-	parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \
-	parsing/g_ltac.cmo parsing/g_constr.cmo parsing/g_cases.cmo \
 	parsing/extend.cmo \
-	parsing/coqlib.cmo library/goptions.cmo pretyping/detyping.cmo \
+	parsing/coqlib.cmo pretyping/detyping.cmo \
 	parsing/termast.cmo parsing/astterm.cmo \
 	parsing/egrammar.cmo parsing/esyntax.cmo toplevel/metasyntax.cmo \
-	parsing/printer.cmo pretyping/typing.cmo \
+	parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo \
+	lib/stamps.cmo pretyping/typing.cmo \
 	proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \
 	proofs/evar_refiner.cmo proofs/tacmach.cmo toplevel/himsg.cmo \
 	parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \
-	toplevel/cerrors.cmo
-
-ML4FILES += contrib/correctness/psyntax.ml4 contrib/field/field.ml4
-
-OMEGACMO=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo
-
-ROMEGACMO=contrib/romega/const_omega.cmo contrib/romega/refl_omega.cmo 
-
-RINGCMO=contrib/ring/quote.cmo contrib/ring/ring.cmo 
+	toplevel/class.cmo toplevel/recordobj.cmo toplevel/cerrors.cmo \
+	parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \
+	parsing/g_ltac.cmo parsing/g_constr.cmo parsing/g_cases.cmo \
+	proofs/tactic_debug.cmo \
+	proofs/pfedit.cmo proofs/clenv.cmo tactics/wcclausenv.cmo \
+	tactics/tacticals.cmo tactics/hipattern.cmo \
+	tactics/tactics.cmo tactics/hiddentac.cmo \
+	tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
+	tactics/nbtermdn.cmo tactics/dhyp.cmo tactics/elim.cmo \
+	tactics/auto.cmo tactics/tacinterp.cmo tactics/extraargs.cmo \
+	$(CMO) # Solution de facilité...
+
+ML4FILES += contrib/correctness/psyntax.ml4 contrib/omega/g_omega.ml4 \
+         contrib/romega/g_romega.ml4 contrib/ring/g_quote.ml4 \
+	 contrib/ring/g_ring.ml4 \
+         contrib/field/field.ml4 contrib/fourier/g_fourier.ml4 \
+	 contrib/extraction/g_extraction.ml4 contrib/xml/xmlentries.ml4
+
+OMEGACMO=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
+         contrib/omega/g_omega.cmo 
+
+ROMEGACMO=contrib/romega/const_omega.cmo contrib/romega/refl_omega.cmo \
+         contrib/romega/g_romega.cmo 
+
+RINGCMO=contrib/ring/quote.cmo contrib/ring/g_quote.cmo \
+	contrib/ring/ring.cmo contrib/ring/g_ring.cmo 
 
 FIELDCMO=contrib/field/field.cmo 
 
 XMLCMO=contrib/xml/xml.cmo \
        contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo 	
 
-FOURIERCMO=contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo 	
+FOURIERCMO=contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo \
+        contrib/fourier/g_fourier.cmo
 
 EXTRACTIONCMO=contrib/extraction/table.cmo\
 	      contrib/extraction/mlutil.cmo\
@@ -213,7 +251,8 @@ EXTRACTIONCMO=contrib/extraction/table.cmo\
 	      contrib/extraction/haskell.cmo \
 	      contrib/extraction/extraction.cmo \
               contrib/extraction/common.cmo \
-	      contrib/extraction/extract_env.cmo
+	      contrib/extraction/extract_env.cmo \
+	      contrib/extraction/g_extraction.cmo
 
 CORRECTNESSCMO=contrib/correctness/pmisc.cmo				\
 	contrib/correctness/peffect.cmo contrib/correctness/prename.cmo	\
@@ -230,6 +269,7 @@ JPROVERCMO=contrib/jprover/opname.cmo \
            contrib/jprover/jtunify.cmo contrib/jprover/jall.cmo \
            contrib/jprover/jprover.cmo
 
+ML4FILES += contrib/jprover/jprover.ml4
 
 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) $(XMLCMO) \
 	$(FOURIERCMO) \
@@ -238,8 +278,8 @@ CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) $(XMLCMO) \
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
 
-CMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \
-    $(PROOFS) $(TACTICS) $(TOPLEVEL) $(HIGHTACTICS) $(CONTRIB)
+CMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING)  \
+    $(PROOFS) $(TACTICS) $(PARSING) $(TOPLEVEL) $(HIGHPARSING) $(HIGHTACTICS) $(CONTRIB)
 CMX=$(CMO:.cmo=.cmx)
 
 ###########################################################################
@@ -288,6 +328,7 @@ scripts/tolink.ml: Makefile
 	echo "let proofs = \""$(PROOFS)"\"" >> $@
 	echo "let tactics = \""$(TACTICS)"\"" >> $@
 	echo "let toplevel = \""$(TOPLEVEL)"\"" >> $@
+	echo "let highparsing = \""$(HIGHPARSING)"\"" >> $@
 	echo "let hightactics = \""$(HIGHTACTICS)" "$(USERTACCMO)"\"" >> $@
 	echo "let contrib = \""$(CONTRIB)"\"" >> $@
 
@@ -316,7 +357,9 @@ proofs: $(PROOFS)
 tactics: $(TACTICS)
 parsing: $(PARSING)
 pretyping: $(PRETYPING)
+highparsing: $(HIGHPARSING)
 toplevel: $(TOPLEVEL)
+hightactics: $(HIGHTACTICS)
 
 # special binaries for debugging
 
@@ -344,7 +387,7 @@ check:: $(BESTCOQTOP)
 
 states:: states/barestate.coq states/initial.coq
 
-SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v syntax/PPTactic.v
+SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v
 
 states/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP)
 	$(BESTCOQTOP) -boot -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq
@@ -361,12 +404,9 @@ theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC)
 
 init: $(INITVO)
 
-EXTRACTIONVO=contrib/extraction/Extraction.vo
+EXTRACTIONVO=
 
-TACTICSVO=tactics/Equality.vo \
-	  tactics/Tauto.vo tactics/Inv.vo \
-          tactics/EAuto.vo tactics/AutoRewrite.vo tactics/Refine.vo \
-	  tactics/EqDecide.vo tactics/Setoid_replace.vo $(EXTRACTIONVO)
+TACTICSVO=$(EXTRACTIONVO)
 
 tactics/%.vo: tactics/%.v states/barestate.coq $(COQC)
 	$(BOOTCOQTOP) -is states/barestate.coq -compile $*
@@ -387,7 +427,8 @@ LOGICVO=theories/Logic/Hurkens.vo          theories/Logic/ProofIrrelevance.vo\
       theories/Logic/Berardi.vo       	     theories/Logic/Eqdep_dec.vo \
       theories/Logic/Decidable.vo            theories/Logic/JMeq.vo
 
-ARITHVO=theories/Arith/Arith.vo         theories/Arith/Gt.vo          \
+ARITHVO=theories/Arith/ArithSyntax.vo \
+	theories/Arith/Arith.vo         theories/Arith/Gt.vo          \
 	theories/Arith/Between.vo       theories/Arith/Le.vo          \
 	theories/Arith/Compare.vo       theories/Arith/Lt.vo          \
 	theories/Arith/Compare_dec.vo   theories/Arith/Min.vo         \
@@ -516,7 +557,7 @@ CORRECTNESSVO=contrib/correctness/Arrays.vo				\
 	contrib/correctness/Tuples.vo
 #	contrib/correctness/ProgramsExtraction.vo			
 
-OMEGAVO = contrib/omega/Omega.vo  	contrib/omega/OmegaSyntax.vo
+OMEGAVO = contrib/omega/Omega.vo
 
 ROMEGAVO = contrib/romega/ReflOmegaCore.vo contrib/romega/ROmega.vo 
 
@@ -529,13 +570,13 @@ RINGVO = contrib/ring/ArithRing.vo      contrib/ring/Ring_normalize.vo \
 FIELDVO = contrib/field/Field_Compl.vo     contrib/field/Field_Theory.vo \
           contrib/field/Field_Tactic.vo    contrib/field/Field.vo
 
-XMLVO = contrib/xml/Xml.vo
+XMLVO = Xml.vo
 
 INTERFACEV0 = contrib/interface/Centaur.vo contrib/interface/vernacrc
 
 FOURIERVO = contrib/fourier/Fourier_util.vo    contrib/fourier/Fourier.vo
 
-JPROVERVO = contrib/jprover/JProver.vo
+JPROVERVO = 
 
 contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE)
 	$(BESTCOQTOP) -boot -byte  $(COQINCLUDES) -compile $*
@@ -544,9 +585,8 @@ contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/init
 	$(BESTCOQTOP) -boot -byte  $(COQINCLUDES) -compile $*
 
 CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
-	    $(CORRECTNESSVO)\
-            $(INTERFACEV0) $(FOURIERVO) \
-	    $(JPROVERVO)
+	    $(CORRECTNESSVO) $(FOURIERVO) \
+	    $(JPROVERVO) $(INTERFACEV0)
 
 $(CONTRIBVO): states/initial.coq
 
@@ -706,9 +746,9 @@ LPLIB = lib/doc.tex $(LIBREP:.cmo=.mli)
 LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli)
 LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli)
 LPPRETYPING = pretyping/doc.tex pretyping/rawterm.mli $(PRETYPING:.cmo=.mli)
-LPPARSING =$(PARSING:.cmo=.mli)
+LPPARSING =$(PARSING:.cmo=.mli) $(HIGHPARSING:.cmo=.mli)
 LPPROOFS = proofs/doc.tex $(PROOFS:.cmo=.mli)
-LPTACTICS = tactics/doc.tex $(TACTICS:.cmo=.mli)
+LPTACTICS = tactics/doc.tex $(TACTICS:.cmo=.mli) $(HIGHTACTICS:.cmo=.mli)
 LPTOPLEVEL = toplevel/doc.tex $(TOPLEVEL:.cmo=.mli)
 LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) \
 	  $(LPPRETYPING) $(LPPROOFS) $(LPTACTICS) $(LPTOPLEVEL)
@@ -741,13 +781,22 @@ tags:
 
 # grammar modules with camlp4
 
-ML4FILES += parsing/lexer.ml4 parsing/q_coqast.ml4 \
+ML4FILES += parsing/lexer.ml4 parsing/q_util.ml4 parsing/q_coqast.ml4 \
             parsing/g_prim.ml4 parsing/pcoq.ml4
 
-GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/dyn.cmo \
-	   lib/hashcons.cmo lib/predicate.cmo kernel/names.cmo \
-	   parsing/coqast.cmo parsing/lexer.cmo \
-	   parsing/pcoq.cmo parsing/q_coqast.cmo parsing/g_prim.cmo
+CAMLP4EXTENSIONS= parsing/tacextend.cmo parsing/vernacextend.cmo 
+
+GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
+	   lib/dyn.cmo lib/options.cmo \
+	   lib/hashcons.cmo lib/predicate.cmo lib/rtree.cmo $(KERNEL) \
+	   library/summary.cmo library/nameops.cmo library/nametab.cmo \
+	   library/libobject.cmo library/lib.cmo library/global.cmo \
+	   library/goptions.cmo pretyping/rawterm.cmo pretyping/evd.cmo \
+	   parsing/coqast.cmo parsing/genarg.cmo \
+	   proofs/tacexpr.cmo proofs/proof_type.cmo parsing/ast.cmo \
+           parsing/lexer.cmo parsing/q_util.cmo parsing/extend.cmo \
+           toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_coqast.cmo \
+           parsing/egrammar.cmo parsing/g_prim.cmo $(CAMLP4EXTENSIONS)
 
 parsing/grammar.cma: $(GRAMMARCMO)
 	$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
@@ -758,7 +807,7 @@ clean::
 ML4FILES +=parsing/g_basevernac.ml4 parsing/g_minicoq.ml4 \
 	   parsing/g_vernac.ml4 parsing/g_proofs.ml4 parsing/g_cases.ml4 \
 	   parsing/g_constr.ml4 parsing/g_tactic.ml4 parsing/g_ltac.ml4 \
-	   parsing/extend.ml4    
+	   parsing/tacextend.ml4 parsing/vernacextend.ml4
 
 # beforedepend:: $(GRAMMARCMO)
 
@@ -920,6 +969,9 @@ depend: beforedepend
 # 5. Finally, we erase the generated .ml files
 	rm -f $(ML4FILESML)
 
+ml4clean::
+	rm -f $(ML4FILESML)
+
 clean::
 	rm -f $(ML4FILESML)
 
diff --git a/TODO b/TODO
index 5dbac9958e..e53d95f8e0 100644
--- a/TODO
+++ b/TODO
@@ -1,10 +1,6 @@
-Distribution:
-
-- faire une passe sur les options de coqtop et coqc
-
 Langage:
 
-- Propager les contraintes arrière dans Cases (cf example doc/Cases.tex)
+Distribution:
 
 Environnement:
 
@@ -12,35 +8,41 @@ Environnement:
 
 Noyau:
 
+Tactic:
+
+- Que contradiction raisonne a isomorphisme pres de False
+
 Vernac:
 
 - Print / Print Proof en fait identiques ; Print ne devrait pas afficher
   les constantes opaques (devrait afficher qqchose comme <opaque>)
 
 Theories:
+
 - Rendre transparent tous les theoremes prouvant {A}+{B}
 - Faire demarrer PolyList.nth a` l'indice 0 
-Renommer l'actuel nth en nth1 ??
-
-Grammaires:
-
-- revoir numarg/pure_numarg dans g_tactic.ml4 (regles a factoriser)
+  Renommer l'actuel nth en nth1 ??
 
 Doc:
 
 - Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
-- Documenter le nouvel Assert x:=t.
 - Documenter le filtrage sur les types inductifs avec let-ins (dont la
-  compatibility V6)
+  compatibilite V6)
 
 - Ajouter let dans les règles du CIC
   -> FAIT, mais reste a documenter le let dans les inductifs
   et les champs manifestes dans les Record   
 - revoir le chapitre sur les tactiques utilisateur 
 - faut-il mieux spécifier la sémantique de Simpl (??)
-- documenter @Definition and co
 
-- Suggestions de la formation
-  Dans le Intros pattern on pourrait interpreter les _ 
-  comme des hypotheses sur lesquelles on ferait Clear immediatement
--> FAIT, semble-t'il
+- Préciser la clarification syntaxique de IntroPattern
+- preciser que Goal vient en dernier dans une clause pattern list et
+  qu'il doit apparaitre si il y a un "in"
+
+- Omega Time debranche mais Omega System et Omega Action remarchent ?
+- Ajout "Replace in" (mais TODO)
+- Syntaxe Conditional tac Rewrite marche, à documenter
+- Documenter Dependent Rewrite et CutRewrite ?
+- Ajouter les motifs sous-termes de ltac
+
+
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index e6f6891f73..ffcb7c648e 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -52,7 +52,7 @@ let tuple_n n =
       (fun i -> 
 	 let id = id_of_string 
 		    ("proj_" ^ string_of_int n ^ "_" ^ string_of_int i) in
-	 (false, (id, true, Ast.nvar (id_of_string ("T" ^ string_of_int i)))))
+	 (false, Vernacexpr.AssumExpr (id, Ast.nvar (id_of_string ("T" ^ string_of_int i)))))
       l1n 
   in
   let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index c7f1fc2ed7..d191b58ebf 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -220,6 +220,14 @@ let reduce_open_constr (em0,c) =
   let em = existential_map_of_constr c in
   (em,c)
 
+let register id n =
+  let id' = match n with None -> id | Some id' -> id' in
+  Penv.register id id'
+
+let correctness_hook _ ref = 
+  let pf_id = Nameops.basename (Nametab.sp_of_global (Global.env()) ref) in
+  register pf_id None
+
 let correctness s p opttac =
   Pmisc.reset_names();
   let p,oc,cty,v = coqast_of_prog p in
@@ -228,14 +236,14 @@ let correctness s p opttac =
   let sigma = Evd.empty in
   let cty = Reduction.nf_betaiota cty in
   let id = id_of_string s in 
-  start_proof id Declare.NeverDischarge sign cty;
+  start_proof id (false,Nametab.NeverDischarge) sign cty correctness_hook;
   Penv.new_edited id (v,p);
   if !debug then show_open_subgoals();
   deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ());
   let oc = reduce_open_constr oc in
   deb_mess (str"AFTER REDUCTION:" ++ fnl ());
   deb_mess (Printer.prterm_env (Global.env()) (snd oc));
-  let tac = (tclTHEN (Refine.refine_tac oc) automatic) in
+  let tac = (tclTHEN (Extratactics.refine_tac oc) automatic) in
   let tac = match opttac with 
     | None -> tac
     | Some t -> tclTHEN tac t
@@ -245,15 +253,11 @@ let correctness s p opttac =
 
 
 (* On redéfinit la commande "Save" pour enregistrer les nouveaux programmes *)
-
+(*
 open Vernacinterp
 
 let add = Vernacinterp.overwriting_vinterp_add
 
-let register id n =
-  let id' = match n with None -> id | Some id' -> id' in
-  Penv.register id id'
-
 let _ = 
   let current_save = Vernacinterp.vinterp_map "SaveNamed" in
   add "SaveNamed"
@@ -282,4 +286,4 @@ let _ =
 	let pf_id = Pfedit.get_current_proof_name () in
 	current_saveanonymous l ();
 	register pf_id (Some id)))
-
+*)
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
deleted file mode 100644
index 0f69bce4a4..0000000000
--- a/contrib/extraction/Extraction.v
+++ /dev/null
@@ -1,86 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-Grammar vernac vernac : ast :=
-
-(* Extraction in the Coq toplevel *)
-  extr_constr [ "Extraction" constrarg($c) "." ] -> 
-              [ (Extraction $c) ]
-| extr_list   [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] ->
-              [ (ExtractionRec ($LIST $l)) ]
-
-(* Monolithic extraction to a file *)
-| extr_file
-     [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] 
-  -> [ (ExtractionFile $f ($LIST $l)) ]
-
-(* Modular extraction (one Coq module = one ML module) *)
-| extr_module 
-     [ "Extraction" "Module" identarg($m) "." ]
-  -> [ (ExtractionModule $m) ]
-| rec_extr_module 
-     [ "Recursive" "Extraction" "Module" identarg($m) "." ]
-  -> [ (RecursiveExtractionModule $m) ]
-
-(* Target Language *)
-
-| extr_language 
-     [ "Extraction" "Language" extraction_language($l) "." ] 
-  -> [ (ExtractionLang $l) ]
-
-(* Custom inlining directives *)
-| inline_constant
-     [ "Extraction" "Inline" ne_qualidarg_list($l) "." ] 
-  -> [ (ExtractionInline ($LIST $l)) ]
-     
-| no_inline_constant 
-     [ "Extraction" "NoInline" ne_qualidarg_list($l) "." ] 
-  -> [ (ExtractionNoInline ($LIST $l)) ]
-
-| print_inline_constant 
-     [ "Print" "Extraction" "Inline" "."]
-  -> [ (PrintExtractionInline) ]
-
-| reset_inline_constant 
-     [ "Reset" "Extraction" "Inline" "."]
-  -> [ (ResetExtractionInline) ]
-
-(* Overriding of a Coq object by an ML one *)
-| extract_constant 
-     [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ]
-  -> [ (ExtractConstant $x $y) ]
-
-| extract_inlined_constant 
-     [ "Extract" "Inlined" "Constant" qualidarg($x) 
-      "=>" idorstring($y) "." ]
-  -> [ (ExtractInlinedConstant $x $y) ]
-
-| extract_inductive 
-     [ "Extract" "Inductive" qualidarg($x) "=>" mindnames($y) "."]
-  -> [ (ExtractInductive $x $y) ]
-
-(* Utility entries *)
-with mindnames : ast :=
-  mlconstr [ idorstring($id) "[" idorstring_list($idl) "]" ]
-        -> [(VERNACARGLIST $id ($LIST $idl))]
-
-with idorstring_list: ast list :=
-  ids_nil  [ ] -> [ ]
-| ids_cons [ idorstring($x) idorstring_list($l) ] -> [ $x ($LIST $l) ]
-
-with idorstring : ast :=
-  ids_ident  [ identarg($id) ] -> [ $id ]
-| ids_string [ stringarg($s) ] -> [ $s ]
-
-with extraction_language : ast := 
-  ocaml [ "Ocaml" ] -> [ "Ocaml" ]
-| haskell [ "Haskell" ] -> [ "Haskell" ]
-| toplevel [ "Toplevel" ] -> [ "Toplevel" ]
-
-.
-
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index ecfd5e2ea8..db2e7d4f93 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -241,40 +241,33 @@ let extract_reference r =
       else List.find (decl_in_r r) decls
       in msgnl (pp_decl d)
 
-let _ = 
-  vinterp_add "Extraction"
-    (function 
-       | [VARG_CONSTR ast] ->
-	   (fun () -> 
-	      set_globals ();
-	      let c = Astterm.interp_constr Evd.empty (Global.env()) ast in
-	      match kind_of_term c with
-		(* If it is a global reference, then output the declaration *)
-		| Const sp -> extract_reference (ConstRef sp)
-		| Ind ind -> extract_reference (IndRef ind)
-		| Construct cs -> extract_reference (ConstructRef cs)
-		(* Otherwise, output the ML type or expression *)
-		| _ ->
-		    match extract_constr (Global.env()) c with
-		      | Emltype (t,_,_) -> msgnl (pp_type t ++ fnl ())
-		      | Emlterm a -> msgnl (pp_ast (normalize a) ++ fnl ()))
-       | _ -> assert false)
+let extraction rawconstr =
+  set_globals ();
+  let c = Astterm.interp_constr Evd.empty (Global.env()) rawconstr in
+  match kind_of_term c with
+    (* If it is a global reference, then output the declaration *)
+    | Const sp -> extract_reference (ConstRef sp)
+    | Ind ind -> extract_reference (IndRef ind)
+    | Construct cs -> extract_reference (ConstructRef cs)
+    (* Otherwise, output the ML type or expression *)
+    | _ ->
+	match extract_constr (Global.env()) c with
+	  | Emltype (t,_,_) -> msgnl (pp_type t ++ fnl ())
+	  | Emlterm a -> msgnl (pp_ast (normalize a) ++ fnl ())
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
     \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env]
     to get the saturated environment to extract. *)
 
 let mono_extraction (f,m) vl = 
-  let refs = refs_of_vargl vl in
+  let refs = List.map Nametab.global vl in
   let prm = {modular=false; mod_name = m; to_appear= refs} in
   let decls = decl_of_refs refs in 
   let decls = add_ml_decls prm decls in 
   let decls = optimize prm decls in
   extract_to_file f prm decls
 
-let _ = 
-  vinterp_add "ExtractionRec"
-    (fun vl () -> mono_extraction (None,id_of_string "Main") vl)
+let extraction_rec = mono_extraction (None,id_of_string "Main")
 
 (*s Extraction to a file (necessarily recursive). 
     The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn].
@@ -297,14 +290,9 @@ let lang_error () =
      ++ fnl () ++
      str "You should use Extraction Language Ocaml or Haskell before.") 
 
-let _ = 
-  vinterp_add "ExtractionFile"
-    (function 
-       | VARG_STRING f :: vl ->
-	   (fun () -> 
-	      if lang () = Toplevel then lang_error () 
-	      else mono_extraction (filename f) vl) 
-       | _ -> assert false)
+let extraction_file f vl =
+  if lang () = Toplevel then lang_error () 
+  else mono_extraction (filename f) vl
 
 (*s Extraction of a module. The vernacular command is 
   \verb!Extraction Module! [M]. *) 
@@ -322,48 +310,37 @@ let module_file_name m = match lang () with
   | Haskell -> (String.capitalize (string_of_id m)) ^ ".hs"
   | Toplevel -> assert false
 
-let _ = 
-  vinterp_add "ExtractionModule"
-    (function 
-       | [VARG_IDENTIFIER m] ->
-	   (fun () -> 
-	      if lang () = Toplevel then lang_error () 
-	      else 
-		let dir_m = module_of_id m in 
-		let f = module_file_name m in
-		let prm = {modular=true; mod_name=m; to_appear=[]} in 
-		let rl = extract_module dir_m in 
-		let decls = optimize prm (decl_of_refs rl) in
-		let decls = add_ml_decls prm decls in 
-		check_one_module dir_m decls; 
-		let decls = List.filter (decl_in_m dir_m) decls in
-		extract_to_file (Some f) prm decls)
-       | _ -> assert false)
+let extraction_module m =
+  if lang () = Toplevel then lang_error () 
+  else 
+    let dir_m = module_of_id m in 
+    let f = module_file_name m in
+    let prm = {modular=true; mod_name=m; to_appear=[]} in 
+    let rl = extract_module dir_m in 
+    let decls = optimize prm (decl_of_refs rl) in
+    let decls = add_ml_decls prm decls in 
+    check_one_module dir_m decls; 
+    let decls = List.filter (decl_in_m dir_m) decls in
+    extract_to_file (Some f) prm decls
 
 (*s Recursive Extraction of all the modules [M] depends on. 
   The vernacular command is \verb!Recursive Extraction Module! [M]. *) 
 
-let _ = 
-  vinterp_add "RecursiveExtractionModule"
-        (function 
-       | [VARG_IDENTIFIER m] ->
-	   (fun () -> 
-	      if lang () = Toplevel then lang_error () 
-	      else 
-		let dir_m = module_of_id m in 
-		let modules,refs = 
-		  modules_extract_env dir_m in
-		check_modules modules; 
-		let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
-		let decls = optimize dummy_prm (decl_of_refs refs) in
-		let decls = add_ml_decls dummy_prm decls in
-		Dirset.iter 
-		  (fun m ->
-		     let short_m = snd (split_dirpath m) in
-		     let f = module_file_name short_m in 
-		     let prm = {modular=true;mod_name=short_m;to_appear=[]} in 
-		     let decls = List.filter (decl_in_m m) decls in
-		     if decls <> [] then extract_to_file (Some f) prm decls)
-		  modules)
-       | _ -> assert false)
-
+let recursive_extraction_module m =
+  if lang () = Toplevel then lang_error () 
+  else 
+    let dir_m = module_of_id m in 
+    let modules,refs = 
+      modules_extract_env dir_m in
+    check_modules modules; 
+    let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
+    let decls = optimize dummy_prm (decl_of_refs refs) in
+    let decls = add_ml_decls dummy_prm decls in
+    Dirset.iter 
+      (fun m ->
+	let short_m = snd (split_dirpath m) in
+	let f = module_file_name short_m in 
+	let prm = {modular=true;mod_name=short_m;to_appear=[]} in 
+	let decls = List.filter (decl_in_m m) decls in
+	if decls <> [] then extract_to_file (Some f) prm decls)
+      modules
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index 710e801d12..1cdb5c02c3 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -10,3 +10,12 @@
 
 (*s This module declares the extraction commands. *)
 
+open Util
+open Names
+open Nametab
+
+val extraction : Genarg.constr_ast -> unit
+val extraction_rec : qualid located list -> unit
+val extraction_file : string -> qualid located list -> unit
+val extraction_module : identifier -> unit
+val recursive_extraction_module : identifier -> unit
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 896203486b..ee7267f3f6 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -13,6 +13,7 @@ open Lib
 open Libobject
 open Goptions
 open Vernacinterp
+open Extend
 open Names
 open Util
 open Pp
@@ -66,21 +67,25 @@ let check_constant r =
   else errorlabstrm "extract_constant"
 	(Printer.pr_global r ++ spc () ++ str "is not a constant.") 
 
+(*
 let string_of_varg = function
   | VARG_IDENTIFIER id -> string_of_id id
   | VARG_STRING s -> s
   | _ -> assert false
+*)
 
 let no_such_reference q =
   errorlabstrm "reference_of_varg" 
     (str "There is no such reference " ++ Nametab.pr_qualid q ++ str ".")
 
+(*
 let reference_of_varg = function
   | VARG_QUALID q -> 
       (try Nametab.locate q with Not_found -> no_such_reference q)
   | _ -> assert false
 
 let refs_of_vargl = List.map reference_of_varg
+*)
 
 (*s Target Language *)
 
@@ -103,18 +108,7 @@ let _ = declare_summary "Extraction Lang"
 	    init_function = (fun () -> lang_ref := Ocaml);
 	    survive_section = true }  
 
-let lang_to_lang = function 
-    "Ocaml" -> Ocaml 
-  | "Haskell" -> Haskell 
-  | "Toplevel" -> Toplevel
-  | _ -> assert false
-
-let _ = 
-  vinterp_add "ExtractionLang" 
-     (function 
-	  [VARG_STRING l] -> 
-	    (fun () -> add_anonymous_leaf (extr_lang (lang_to_lang l)))
-	| _ -> assert false)
+let extraction_language x = add_anonymous_leaf (extr_lang x)
 
 (*s Table for custom inlining *)
 
@@ -150,21 +144,13 @@ let _ = declare_summary "Extraction Inline"
 
 (*s Grammar entries. *)
 
-let _ = 
-  vinterp_add "ExtractionInline"
-    (fun vl () -> 
-       let refs = List.map check_constant (refs_of_vargl vl) in 
-       add_anonymous_leaf (inline_extraction (true,refs)))
-
-let _ = 
-  vinterp_add "ExtractionNoInline"
-    (fun vl () -> 
-       let refs = List.map check_constant (refs_of_vargl vl) in 
-       add_anonymous_leaf (inline_extraction (false,refs)))
+let extraction_inline b vl =
+  let refs = List.map (fun x -> check_constant (Nametab.global x)) vl in 
+  add_anonymous_leaf (inline_extraction (true,refs))
 
 (*s Printing part *)
 
-let print_inline () = 
+let print_extraction_inline () = 
   let (i,n)= !inline_table in 
   let i'= Refset.filter is_constant i in 
   msg 
@@ -177,9 +163,6 @@ let print_inline () =
        (fun r p -> 
 	  (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) n (mt ()))
 
-let _ = vinterp_add "PrintExtractionInline" (fun _ -> print_inline)
-
-
 (*s Reset part *)
 
 let (reset_inline,_) = 
@@ -189,10 +172,8 @@ let (reset_inline,_) =
 	load_function = (fun (_,_)-> inline_table :=  empty_inline_table); 
 	open_function = (fun _ -> ());
 	export_function = (fun x -> Some x) })
-	
-let _ = vinterp_add "ResetExtractionInline" 
-	  (fun _ () -> add_anonymous_leaf (reset_inline ()))
-	  
+
+let reset_extraction_inline () = add_anonymous_leaf (reset_inline ())
 
 (*s Table for direct ML extractions. *)
 
@@ -235,30 +216,13 @@ let _ = declare_summary "ML extractions"
 
 (*s Grammar entries. *)
 
-let _ = 
-  vinterp_add "ExtractConstant"
-    (function 
-       | [id; vs] -> 
-	   (fun () -> 
-	      let r = check_constant (reference_of_varg id) in 
-	      let s = string_of_varg vs in 
-	      add_anonymous_leaf (inline_extraction (false,[r]));
-	      add_anonymous_leaf (in_ml_extraction (r,s)))
-       | _ -> assert false)
-
-let _ = 
-  vinterp_add "ExtractInlinedConstant"
-    (function 
-       | [id; vs] -> 
-	   (fun () -> 
-	      let r = check_constant (reference_of_varg id) in 
-	      let s = string_of_varg vs in 
-	      add_anonymous_leaf (inline_extraction (true,[r]));
-	      add_anonymous_leaf (in_ml_extraction (r,s)))
-       | _ -> assert false)
-
-
-let extract_inductive r (id2,l2) = match r with
+let extract_constant_inline inline qid s =
+  let r = check_constant (Nametab.global qid) in
+  add_anonymous_leaf (inline_extraction (inline,[r]));
+  add_anonymous_leaf (in_ml_extraction (r,s))
+
+let extract_inductive r (id2,l2) =
+  let r = Nametab.global r in match r with
   | IndRef ((sp,i) as ip) ->
       let mib = Global.lookup_mind sp in
       let n = Array.length mib.mind_packets.(i).mind_consnames in
@@ -273,13 +237,3 @@ let extract_inductive r (id2,l2) = match r with
   | _ -> 
       errorlabstrm "extract_inductive"
 	(Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
-
-let _ = 
-  vinterp_add "ExtractInductive"
-    (function 
-       | [q1; VARG_VARGLIST (id2 :: l2)] ->
-	   (fun () -> 
-	      extract_inductive (reference_of_varg q1) 
-		(string_of_varg id2, List.map string_of_varg l2))
-       | _ -> assert false)
-
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index a6cde3c5f2..9fa7142ce8 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -28,7 +28,7 @@ module Refset : Set.S with type elt = global_reference
 		      
 val check_constant : global_reference -> global_reference
 
-val refs_of_vargl : vernac_arg list -> global_reference list
+(*val refs_of_vargl : Extend.vernac_arg list -> global_reference list*)
 
 (*s Target language. *)
 
@@ -52,3 +52,18 @@ val ml_extractions : unit -> Refset.t
 
 val sorted_ml_extractions : unit -> (global_reference * string) list
 
+(*s Extraction commands. *)
+
+open Util
+
+val extraction_language : lang -> unit
+
+val extraction_inline : bool -> qualid located list -> unit
+
+val print_extraction_inline : unit -> unit
+
+val reset_extraction_inline : unit -> unit
+
+val extract_constant_inline : bool -> qualid located -> string -> unit
+
+val extract_inductive : qualid located -> string * string list -> unit
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 74a58b11d4..c877dc47bb 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -18,8 +18,10 @@ open Term
 open Tactics
 open Clenv
 open Names
+open Tacticals
 open Tacmach
 open Fourier
+open Contradiction
 
 (******************************************************************************
 Opérations sur les combinaisons linéaires affines.
@@ -68,6 +70,7 @@ let flin_emult a f =
 ;;
     
 (*****************************************************************************)
+open Vernacexpr
 let parse_ast   = Pcoq.parse_string Pcoq.Constr.constr;;
 let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);;
 let pf_parse_constr gl s =
@@ -550,10 +553,11 @@ let rec fourier gl=
 
 ;;
 
+(*
 let fourier_tac x gl =
      fourier gl
 ;;
 
 let v_fourier = add_tactic "Fourier" fourier_tac
-
+*)
 
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 6df04bd37d..a8b9651148 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -28,6 +28,7 @@ open Declarations
 open Environ
 open Sign
 open Inductive
+open Tacticals
 open Tacmach
 open Evar_refiner
 open Tactics
@@ -35,6 +36,7 @@ open Clenv
 open Logic
 open Nametab
 open Omega
+open Contradiction
 
 (* Added by JCF, 09/03/98 *)
 
@@ -48,6 +50,46 @@ let display_system_flag = ref false
 let display_action_flag = ref false
 let old_style_flag = ref false
 
+let read f () = !f
+let write f x = f:=x
+
+open Goptions
+
+(* Obsolete, subsumed by Time Omega
+let _ =
+  declare_bool_option 
+    { optsync  = false;
+      optname  = "Omega time displaying flag";
+      optkey   = SecondaryTable ("Omega","Time");
+      optread  = read display_time_flag;
+      optwrite = write display_time_flag }
+*)
+
+let _ =
+  declare_bool_option 
+    { optsync  = false;
+      optname  = "Omega system time displaying flag";
+      optkey   = SecondaryTable ("Omega","System");
+      optread  = read display_system_flag;
+      optwrite = write display_system_flag }
+
+let _ =
+  declare_bool_option 
+    { optsync  = false;
+      optname  = "Omega action display flag";
+      optkey   = SecondaryTable ("Omega","Action");
+      optread  = read display_action_flag;
+      optwrite = write display_action_flag }
+
+let _ =
+  declare_bool_option 
+    { optsync  = false;
+      optname  = "Omega old style flag";
+      optkey   = SecondaryTable ("Omega","OldStyle");
+      optread  = read old_style_flag;
+      optwrite = write old_style_flag }
+
+
 let all_time        = timing "Omega     "
 let solver_time     = timing "Solver    "
 let exact_time      = timing "Rewrites  "
@@ -70,7 +112,8 @@ let new_identifier_var =
 let rec mk_then = 
   function [t] -> t | (t::l) -> (tclTHEN (t) (mk_then l)) | [] -> tclIDTAC
 
-let exists_tac c = constructor_tac (Some 1) 1 [Com,c]
+let exists_tac c = constructor_tac (Some 1) 1 (Rawterm.ImplicitBindings [c])
+
 let generalize_tac t = generalize_time (generalize t)
 let elim t = elim_time (simplest_elim t)
 let exact t = exact_time (Tactics.refine t)
@@ -1822,7 +1865,3 @@ let omega_solver gl =
   (* if !display_time_flag then begin text_time (); 
      flush Pervasives.stdout end; *)
   result
-
-let omega = hide_atomic_tactic "Omega" omega_solver
-
-
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 669fd21c50..bcd8ee5f94 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -112,7 +112,7 @@ open Pattern
 open Tacmach
 open Tactics
 open Proof_trees
-open Proof_type
+open Tacexpr
 (*i*)
 
 (*s First, we need to access some Coq constants
@@ -452,18 +452,6 @@ let quote f lid gl =
     | None -> Tactics.convert_concl (mkApp (f, [| p |])) gl
     | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) gl
 
-(*i*)
-let dyn_quote = function
-  | [Identifier f] -> quote f []
-  | Identifier f :: lid -> quote f 
-        (List.map (function 
-		     | Identifier id -> id 
-		     | other -> bad_tactic_args "Quote" [other]) lid)
-  | l -> bad_tactic_args "Quote" l
-
-let h_quote = hide_tactic "Quote" dyn_quote
-(*i*)
-
 (*i 
 
 Just testing ...
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index e6635c441b..25c3f74917 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -17,12 +17,14 @@ open Term
 open Names
 open Nameops
 open Reductionops
+open Tacticals
+open Tacexpr
 open Tacmach
-open Proof_type
 open Proof_trees
 open Printer
 open Equality
 open Vernacinterp
+open Vernacexpr
 open Libobject
 open Closure
 open Tacred
@@ -227,34 +229,34 @@ let unbox = function
 
 (* Add a Ring or a Semi-Ring to the database after a type verification *)
 
+let implement_theory env t th args =
+  is_conv env Evd.empty (Typing.type_of env Evd.empty t) (mkLApp (th, args))
+
 let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset = 
   if theories_map_mem a then errorlabstrm "Add Semi Ring" 
     (str "A (Semi-)(Setoid-)Ring Structure is already declared for " ++
        prterm a);
   let env = Global.env () in
     if (want_ring & want_setoid &
-	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
-		(mkLApp (coq_Setoid_Ring_Theory, 
-			[| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|])))) &
-	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty (unbox asetth))
-		(mkLApp (coq_Setoid_Theory, [| a; (unbox aequiv) |]))))) then 
+	not (implement_theory env t coq_Setoid_Ring_Theory
+	  [| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|])
+        &
+	not (implement_theory env (unbox asetth) coq_Setoid_Theory
+	  [| a; (unbox aequiv) |])) then 
       errorlabstrm "addring" (str "Not a valid Setoid-Ring theory");
     if (not want_ring & want_setoid &
-	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
-		(mkLApp (coq_Semi_Setoid_Ring_Theory, 
-			[| a; (unbox aequiv); aplus; amult; aone; azero; aeq|])))) &
-	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty (unbox asetth))
-		(mkLApp (coq_Setoid_Theory, [| a; (unbox aequiv) |]))))) then 
+        not (implement_theory env t coq_Semi_Setoid_Ring_Theory 
+	  [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|]) &
+	not (implement_theory env (unbox asetth) coq_Setoid_Theory
+	  [| a; (unbox aequiv) |])) then 
       errorlabstrm "addring" (str "Not a valid Semi-Setoid-Ring theory");
     if (want_ring & not want_setoid &
-	not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
-	       (mkLApp (coq_Ring_Theory, 
-		       [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])))) then
+	not (implement_theory env t coq_Ring_Theory
+	  [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])) then
       errorlabstrm "addring" (str "Not a valid Ring theory");
     if (not want_ring & not want_setoid &
-	not (is_conv  env Evd.empty (Typing.type_of env Evd.empty t) 
-	       (mkLApp (coq_Semi_Ring_Theory, 
-		       [| a; aplus; amult; aone; azero; aeq |])))) then 
+	not (implement_theory env t coq_Semi_Ring_Theory
+	  [| a; aplus; amult; aone; azero; aeq |])) then 
       errorlabstrm "addring" (str "Not a valid Semi-Ring theory");
     Lib.add_anonymous_leaf
       (theory_to_obj 
@@ -274,151 +276,6 @@ let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus
 	       th_t = t;
 	       th_closed = cset }))
 
-(* The vernac commands "Add Ring" and "Add Semi Ring" *)
-(* see file Ring.v for examples of this command *)
-
-let constr_of_comarg = function 
-  | VARG_CONSTR c -> constr_of c
-  | _ -> anomaly "Add (Semi) (Setoid) Ring"
-  
-let cset_of_comarg_list l = 
-  List.fold_right ConstrSet.add (List.map constr_of_comarg l) ConstrSet.empty
-
-let _ = 
-  vinterp_add "AddSemiRing"
-    (function
-       | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
-	 ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aeq)
-	 ::(VARG_CONSTR t)::l -> 
-	   (fun () -> (add_theory false false false
-			 (constr_of a)
-			 None
-			 None
-			 None
-			 (constr_of aplus)
-			 (constr_of amult)
-			 (constr_of aone)
-			 (constr_of azero)
-			 None
-			 (constr_of aeq)
-			 (constr_of t)
-			 (cset_of_comarg_list l)))
-       | _ -> anomaly "AddSemiRing")
-
-let _ = 
-  vinterp_add "AddRing"
-    (function 
-       | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
-	 ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp)
-	 ::(VARG_CONSTR aeq)::(VARG_CONSTR t)::l -> 
-	   (fun () -> (add_theory true false false
-			 (constr_of a)
-			 None
-			 None
-			 None
-			 (constr_of aplus)
-			 (constr_of amult)
-			 (constr_of aone)
-			 (constr_of azero)
-			 (Some (constr_of aopp))
-			 (constr_of aeq)
-			 (constr_of t)
-			 (cset_of_comarg_list l)))
-       | _ -> anomaly "AddRing")
-    
-let _ = 
-  vinterp_add "AddSetoidRing"
-    (function 
-       | (VARG_CONSTR a)::(VARG_CONSTR aequiv)::(VARG_CONSTR asetth)::(VARG_CONSTR aplus)
-	 ::(VARG_CONSTR amult)::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp)
-	 ::(VARG_CONSTR aeq)::(VARG_CONSTR pm)::(VARG_CONSTR mm)::(VARG_CONSTR om)
-	 ::(VARG_CONSTR t)::l -> 
-	   (fun () -> (add_theory true false true
-			 (constr_of a)
-			 (Some (constr_of aequiv))
-			 (Some (constr_of asetth))
-			 (Some {
-			    plusm = (constr_of pm);
-			    multm = (constr_of mm);
-			    oppm = Some (constr_of om)})
-			 (constr_of aplus)
-			 (constr_of amult)
-			 (constr_of aone)
-			 (constr_of azero)
-			 (Some (constr_of aopp))
-			 (constr_of aeq)
-			 (constr_of t)
-			 (cset_of_comarg_list l)))
-       | _ -> anomaly "AddSetoidRing")
-    
-let _ = 
-  vinterp_add "AddSemiSetoidRing"
-    (function 
-       | (VARG_CONSTR a)::(VARG_CONSTR aequiv)::(VARG_CONSTR asetth)::(VARG_CONSTR aplus)
-	 ::(VARG_CONSTR amult)::(VARG_CONSTR aone)::(VARG_CONSTR azero)
-	 ::(VARG_CONSTR aeq)::(VARG_CONSTR pm)::(VARG_CONSTR mm)
-	 ::(VARG_CONSTR t)::l -> 
-	   (fun () -> (add_theory false false true
-			 (constr_of a)
-			 (Some (constr_of aequiv))
-			 (Some (constr_of asetth))
-			 (Some {
-			    plusm = (constr_of pm);
-			    multm = (constr_of mm);
-			    oppm = None})
-			 (constr_of aplus)
-			 (constr_of amult)
-			 (constr_of aone)
-			 (constr_of azero)
-			 None
-			 (constr_of aeq)
-			 (constr_of t)
-			 (cset_of_comarg_list l)))
-       | _ -> anomaly "AddSemiSetoidRing")
-    
-let _ = 
-  vinterp_add "AddAbstractSemiRing"
-    (function 
-       | [VARG_CONSTR a; VARG_CONSTR aplus; 
-	  VARG_CONSTR amult; VARG_CONSTR aone;
-	  VARG_CONSTR azero; VARG_CONSTR aeq; VARG_CONSTR t] -> 
-	   (fun () -> (add_theory false true false
-			 (constr_of a)
-			 None
-			 None
-			 None
-			 (constr_of aplus)
-			 (constr_of amult)
-			 (constr_of aone)
-			 (constr_of azero)
-			 None
-			 (constr_of aeq)
-			 (constr_of t)
-			 ConstrSet.empty))
-       | _ -> anomaly "AddAbstractSemiRing")
-    
-let _ = 
-  vinterp_add "AddAbstractRing"
-    (function 
-       | [ VARG_CONSTR a; VARG_CONSTR aplus; 
-	   VARG_CONSTR amult; VARG_CONSTR aone;
-	   VARG_CONSTR azero; VARG_CONSTR aopp; 
-	   VARG_CONSTR aeq; VARG_CONSTR t ] -> 
-	   (fun () -> (add_theory true true false
-			 (constr_of a)
-			 None
-			 None
-			 None
-			 (constr_of aplus)
-			 (constr_of amult)
-			 (constr_of aone)
-			 (constr_of azero)
-			 (Some (constr_of aopp))
-			 (constr_of aeq)
-			 (constr_of t)
-			 ConstrSet.empty))
-       | _ -> anomaly "AddAbstractRing")
-    
 (******** The tactic itself *********)
 
 (*
@@ -894,14 +751,13 @@ let guess_eq_tac th =
         (tclTHEN
 	   (* Normalized sums associate on the right *)
 	   (tclREPEAT
-	      (tclTHENST
+	      (tclTHENFIRST
 		 (apply (mkApp(build_coq_f_equal2 (),
 		               [| th.th_a; th.th_a; th.th_a;
 				  th.th_plus |])))
-		 [reflexivity]
-		 tclIDTAC))
+		 reflexivity))
 	   (tclTRY
-	      (tclTHENL
+	      (tclTHENLAST
 		 (apply (mkApp(build_coq_f_equal2 (),
 			       [| th.th_a; th.th_a; th.th_a;
 				  th.th_plus |])))
@@ -964,13 +820,3 @@ let polynom lc gl =
 	    errorlabstrm "Ring :"
 	      (str" All terms must have the same type");
 	  (tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl
-
-let dyn_polynom ltacargs gl =  
-  polynom (List.map 
-	     (function 
-		| Command c -> pf_interp_constr gl c 
-		| Constr c -> c 
-		| _ -> anomaly "dyn_polynom")
-	     ltacargs) gl
-
-let v_polynom = add_tactic "Ring" dyn_polynom
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index 9ff41f0b52..788d3338cf 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -596,7 +596,9 @@ let coq_omega gl =
   with Omega.NO_CONTRADICTION -> Util.error "Omega can't solve this system"
   end
 
+(*
 let refl_omega = Tacmach.hide_atomic_tactic "StepOmega" coq_omega 
+*)
 
 (* \section{Encapsulation ROMEGA} *)
 
@@ -614,6 +616,7 @@ open Term
 open Environ
 open Sign
 open Inductive
+open Tacticals
 open Tacmach
 open Tactics
 open Tacticals
@@ -832,5 +835,7 @@ let omega_solver gl =
   in
   (loop concl) gl
 
+(*
 let omega = hide_atomic_tactic "ReflOmega" omega_solver
+*)
 
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
index 6d8250ef76..07335ea6a5 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/contrib/xml/xmlcommand.mli
@@ -28,7 +28,7 @@
 (* Note: it is printed only (and directly) the most cooked available      *)
 (*       form of the definition (all the parameters are                   *)
 (*       lambda-abstracted, but the object can still refer to variables)  *)
-val print : Nametab.qualid -> string option -> unit
+val print : Nametab.qualid Util.located -> string option -> unit
 
 (* show dest                                                  *)
 (*  where dest is either None (for stdout) or (Some filename) *)
@@ -46,7 +46,7 @@ val printAll : unit -> unit
 (* and terms of the module d                                                 *)
 (* Note: the terms are printed in their uncooked form plus the informations  *)
 (* on the parameters of their most cooked form                               *)
-val printModule : Nametab.qualid -> string option -> unit
+val printModule : Nametab.qualid Util.located -> string option -> unit
 
 (* printSection identifier directory_name *)
 (*  where identifier     is the name of a closed section d                   *)
diff --git a/dev/changements.txt b/dev/changements.txt
index 29eab892e8..a294082f75 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -1,3 +1,45 @@
+MAIN CHANGES FROM COQ V7.3
+==========================
+
+New parsing model for tactics and vernacular commands
+
+  - Introduction of a dedicated type for tactic expressions
+    (Tacexpr.raw_tactic_expr)
+  - Introduction of a dedicated type for vernac expressions
+    (Vernacexpr.vernac_expr)
+  - Declaration of new vernacular parsing rules by a new camlp4 macro
+    GRAMMAR COMMAND EXTEND ... END  to be used in ML files
+  - Declaration of new tactics parsing/printing rules by a new camlp4 macro
+    TACTIC EXTEND ... END  to be used in ML files
+
+New organisation of THENS:
+tclTHENS tac tacs : tacs is now an array
+tclTHENSFIRSTn tac1 tacs tac2 :
+  apply tac1 then, apply the array tacs on the first n subgoals and
+  tac2 on the remaining subgoals (previously tclTHENST)
+tclTHENSLASTn tac1 tac2 tacs :
+  apply tac1 then, apply tac2 on the first subgoals and apply the array
+  tacs on the last n subgoals
+tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI)
+tclTHENLASTn tac1 tacs  = tclTHENSLASTn tac1 tclIDTAC tacs
+tclTHENFIRST tac1 tac2  = tclTHENFIRSTn tac1 [|tac2|]
+tclTHENLAST tac1 tac2   = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL)
+tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number")
+tclTHENSV same as tclTHENS but with an array
+tclTHENSi : no longer available
+
+Proof_type: subproof field in type proof_tree glued with the ref field
+
+Tacmach: no more echo from functions of module Refiner
+
+Files contrib/*/g_*.ml4 take the place of files contrib/*/*.v.
+Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd
+  VERNAC COMMAND EXTEND macros
+File syntax/PPTactic.v moved to parsing/pptactic.ml
+Tactics about False and not now in tactics/contradiction.ml
+Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v)
+File tacinterp.ml moved from proofs to directory tactics
+
 MAIN CHANGES FROM COQ V7.1 TO COQ V7.2
 ======================================
 
diff --git a/dev/db_printers.ml b/dev/db_printers.ml
index c7857e968f..3e4ba263f9 100644
--- a/dev/db_printers.ml
+++ b/dev/db_printers.ml
@@ -8,7 +8,7 @@
 open Pp
 open Names
 
-let pP s = pP (hov 0 s)
+let pp s = pp (hov 0 s)
 
 let prid id = Format.print_string (string_of_id id)
 let prsp sp = Format.print_string (string_of_path sp)
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b179428845..417bbfce2b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -79,7 +79,7 @@ let pp_universes u = pp (str"[" ++ pr_universes u ++ str"]")
 
 let ppenv e = pp (pr_rel_context e (rel_context e))
 
-let pptac = (fun x -> pp(gentacpr x))
+let pptac = (fun x -> pp(Pptactic.pr_raw_tactic x))
 
 let cnt = ref 0
 
diff --git a/doc/newsyntax.tex b/doc/newsyntax.tex
index eb005520d3..035d3d8bd2 100644
--- a/doc/newsyntax.tex
+++ b/doc/newsyntax.tex
@@ -676,4 +676,10 @@ Remplacer Save. par Qed.
 
 Remplacer Implicit Arguments On/Off par Set/Unset Implicit Arguments.
 
+La syntaxe \verb=Intros (a,b)= est inutile, \verb=Intros [a b]= fait l'affaire.
+
+Mettre des \verb=?x= plutot que des \verb=?1= dans les motifs de ltac ??
+
+Virer \verb=Goal= sans argument (synonyme de \verb=Proof= et sans effets).
+
 \end{document}
diff --git a/parsing/extend.ml4 b/parsing/extend.ml4
deleted file mode 100644
index e54ac11bba..0000000000
--- a/parsing/extend.ml4
+++ /dev/null
@@ -1,303 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
-(*i $Id$ i*)
-
-open Util
-open Gramext
-open Pp
-open Pcoq
-open Coqast
-open Ast
-
-(* Converting and checking grammar command *)
-
-type nonterm =
-  | NtShort of string
-  | NtQual of string * string
-
-type prod_item =
-  | Term of Token.pattern
-  | NonTerm of nonterm * entry_type * string option
-
-type grammar_rule = {
-  gr_name : string; 
-  gr_production : prod_item list; 
-  gr_action : Ast.act }
-
-type grammar_entry = { 
-  ge_name : string;
-  ge_type : entry_type;
-  gl_assoc : g_assoc option;
-  gl_rules : grammar_rule list }
-
-type grammar_command = { 
-  gc_univ : string; 
-  gc_entries : grammar_entry list }
-
-let is_ident_not_keyword s =
-  match s.[0] with
-    | 'a'..'z' | 'A'..'Z' | '_' -> not (Lexer.is_keyword s)
-    | _ -> false
-
-let is_number s =
-  match s.[0] with
-    | '0'..'9' -> true
-    | _ -> false
-
-let strip s =
-  let len =
-    let rec loop i len =
-      if i = String.length s then len
-      else if s.[i] == ' ' then loop (i + 1) len
-      else loop (i + 1) (len + 1)
-    in
-    loop 0 0
-  in
-  if len == String.length s then s
-  else
-    let s' = String.create len in
-    let rec loop i i' =
-      if i == String.length s then s'
-      else if s.[i] == ' ' then loop (i + 1) i'
-      else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end
-    in
-    loop 0 0
-
-let terminal s =
-  let s = strip s in
-  if s = "" then failwith "empty token";
-  if is_ident_not_keyword s then ("IDENT", s)
-  else if is_number s then ("INT", s)
-  else ("", s)
-
-
-
-let qualified_nterm current_univ ntrm =
-  match ntrm with
-      NtQual (univ, en) -> (get_univ univ, en)
-    | NtShort en -> (current_univ, en)
-
-(* For compatibility *)
-let rename_command nt =
-  if String.length nt >= 7 & String.sub nt 0 7 = "command"
-  then "constr"^(String.sub nt 7 (String.length nt - 7))
-  else if nt = "lcommand" then "lconstr"
-  else if nt = "lassoc_command4" then "lassoc_constr4"
-  else nt
-
-let nterm univ ast =
-
-  let nont =
-    match ast with
-      | Node (_, "QUAL", [Id (_, u); Id (_, nt)]) ->
-	  NtQual (rename_command u, rename_command nt)
-      | Id (_, nt) -> NtShort (rename_command nt)
-      | _ -> invalid_arg_loc (Ast.loc ast, "Extend.nterm") 
-  in
-  let (u,n) = qualified_nterm univ nont in
-  let e =
-    try 
-      get_entry u n
-    with UserError _ -> 
-      user_err_loc(loc ast,"Externd.nterm", str"unknown grammar entry")
-  in
-  (nont, type_of_entry e)
-
-let prod_item univ env ast =
-  match ast with
-    | Str (_, s) -> env, Term (terminal s)
-    | Node (_, "NT", [nt; Nmeta (locp, p)]) ->
-	let (nont, etyp) = nterm univ nt in
-	((p, etyp) :: env, NonTerm (nont, etyp, Some p))
-    | Node (_, "NT", [nt]) ->
-	let (nont, etyp) = nterm univ nt in 
-	env, NonTerm (nont, etyp, None)
-    | _ -> invalid_arg_loc (Ast.loc ast, "Extend.prod_item")
-
-let rec prod_item_list univ penv pil =
-  match pil with
-    | [] -> [], penv
-    | pi :: pitl ->
-	let (env, pic) = prod_item univ penv pi in
-	let (pictl, act_env) = prod_item_list univ env pitl in
-        (pic :: pictl, act_env)
-
-let gram_rule univ etyp ast =
-  match ast with
-    | Node (_, "GRAMMARRULE", (Id (_, name) :: act :: pil)) ->
-	let (pilc, act_env) = prod_item_list univ [] pil in
-	let a = Ast.to_act_check_vars act_env etyp act in
-        { gr_name=name; gr_production=pilc; gr_action=a }
-    | _ -> invalid_arg_loc (Ast.loc ast, "Extend.gram_rule")
-
-let gram_entry univ (nt, etyp, ass, rl) =
-  { ge_name = nt;
-    ge_type = etyp;
-    gl_assoc = ass;
-    gl_rules = List.map (gram_rule univ etyp) rl }
-
-let gram_assoc = function
-  | Node (_, "LEFTA", []) -> Some LeftA
-  | Node (_, "RIGHTA", []) -> Some RightA
-  | Node (_, "NONA", []) -> Some NonA
-  | Node (_, "NONE", []) -> None
-  | ast -> invalid_arg_loc (Ast.loc ast, "Egrammar.assoc")
-
-let gram_define_entry univ = function
-  | Node (_, "GRAMMARENTRY", (Id (ntl, nt) :: et :: ass :: rl)) ->
-      let etyp = entry_type et in
-      let assoc = gram_assoc ass in
-
-      (* For compatibility *)
-      let nt = rename_command nt in
-
-      let _ =
-        try 
-	  create_entry univ nt etyp
-        with Failure s ->
-          user_err_loc (ntl,"gram_define_entry", str s)
-      in 
-      (nt, etyp, assoc, rl)
-  | ast -> invalid_arg_loc (Ast.loc ast, "gram_define_entry")
-
-let interp_grammar_command univ astl =
-
-      (* For compatibility *)
-      let univ = rename_command univ in
-
-  let u = get_univ univ in
-  let entryl = List.map (gram_define_entry u) astl in
-  { gc_univ = univ;
-    gc_entries = List.map (gram_entry u) entryl }
-
-
-(* Converting and checking pretty-printing command *)
-
-type precedence = int * int * int
-type parenRelation = L | E | Any | Prec of precedence
-
-let compare_prec (a1,b1,c1) (a2,b2,c2) =
-  match (a1=a2),(b1=b2),(c1=c2) with
-    | true,true,true -> 0
-    | true,true,false -> c1-c2
-    | true,false,_ -> b1-b2
-    | false,_,_ -> a1-a2
-
-let tolerable_prec oparent_prec_reln (_,child_prec) =
-  match oparent_prec_reln with
-    | Some ((_,pprec), L) -> (compare_prec child_prec pprec) < 0
-    | Some ((_,pprec), E) -> (compare_prec child_prec pprec) <= 0
-    | Some (_, Prec level) -> (compare_prec child_prec level) <= 0
-    | _ -> true
-
-type ppbox =
-  | PpHB of int
-  | PpHOVB of int
-  | PpHVB of int
-  | PpVB of int
-  | PpTB
-
-type tolerability = (string * precedence) * parenRelation
-
-type unparsing_hunk = 
-  | PH of Ast.pat * string option * parenRelation
-  | RO of string
-  | UNP_BOX of ppbox * unparsing_hunk list
-  | UNP_BRK of int * int
-  | UNP_TBRK of int * int
-  | UNP_TAB
-  | UNP_FNL
-
-let ppcmd_of_box = function
-  | PpHB n -> h n
-  | PpHOVB n -> hov n
-  | PpHVB n -> hv n
-  | PpVB n -> v n
-  | PpTB   -> t
-
-(* Parsing the unparsing specifications *)
-
-let box_of_ast = function
-  | Node (_, "PpHB", [Num (_, n)]) -> (PpHB n)
-  | Node (_, "PpHOVB", [Num (_, n)]) -> (PpHOVB n)
-  | Node (_, "PpHVB", [Num (_, n)]) -> (PpHVB n)
-  | Node (_, "PpVB", [Num (_, n)]) -> (PpVB n)
-  | Node (_, "PpTB", [])           -> PpTB
-  | p -> invalid_arg_loc (Ast.loc p,"Syntaxext.box_of_ast")
-
-let prec_of_ast = function
-  | Node(_,"PREC",[Num(_,a1); Num(_,a2); Num(_,a3)]) -> (a1,a2,a3)
-  | ast -> invalid_arg_loc (Ast.loc ast,"Syntaxext.prec_of_ast")
-
-let extern_of_ast loc = function
-  | [Str(_,ppextern)] -> (ppextern, Any)
-  | [Str(_,ppextern);p] ->
-      (ppextern, Prec (prec_of_ast p))
-  |  _ -> invalid_arg_loc (loc,"Syntaxext.extern_of_ast")
-
-let rec unparsing_hunk_of_ast vars = function
-  | Node(_, "PH", [e; Node (loc,"EXTERN", ext_args)]) ->
-      let (ppex, rel) = extern_of_ast loc ext_args in
-      PH (Ast.val_of_ast vars e, Some ppex, rel)
-  | Node(loc, "PH", [e; Node(_,pr, [])]) ->
-      let reln =
-        (match pr with
-           | "L" -> L
-           | "E" -> E
-           | "Any" -> Any
-           | _ -> invalid_arg_loc (loc,"Syntaxext.paren_reln_of_ast")) in
-      PH (Ast.val_of_ast vars e, None, reln)
-  | Node (_, "RO", [Str(_,s)]) -> RO s
-  | Node (_, "UNP_FNL", []) -> UNP_FNL
-  | Node (_, "UNP_TAB", []) -> UNP_TAB
-  | Node (_, "UNP_BRK", [Num(_, n1); Num(_, n2)]) -> UNP_BRK(n1,n2)
-  | Node (_, "UNP_TBRK", [Num(_, n1); Num(_, n2)]) -> UNP_TBRK(n1,n2)
-  | Node (_, "UNP_BOX", (box::sub)) ->
-      UNP_BOX(box_of_ast box,
-              List.map (unparsing_hunk_of_ast vars) sub)
-  | h -> invalid_arg_loc (Ast.loc h,"Syntaxext.unparsing_hunk_of_ast")
-
-let unparsing_of_ast vars = function
-  | Node(_,"UNPARSING",ll) ->
-      List.map (unparsing_hunk_of_ast vars) ll
-  | u -> invalid_arg_loc (Ast.loc u,"Syntaxext.unp_of_ast")
-
-type syntax_entry = {
-  syn_id : string;
-  syn_prec: precedence;
-  syn_astpat : Ast.pat;
-  syn_hunks : unparsing_hunk list }
-
-type syntax_command = { 
-  sc_univ : string; 
-  sc_entries : syntax_entry list }
-
-let rule_of_ast whatfor prec = function
-  | Node(_,"SYNTAXRULE",[Id(_,s); spat; unp]) ->
-      let (astpat,meta_env) = Ast.to_pat [] spat in
-      let hunks = unparsing_of_ast meta_env unp in
-      { syn_id = s;
-	syn_prec = prec;
-        syn_astpat = astpat;
-        syn_hunks = hunks }
-  | ast -> invalid_arg_loc (Ast.loc ast,"Metasyntax.rule_of_ast")
-
-let level_of_ast whatfor = function
-  | Node(_,"SYNTAXENTRY",(pr::rl)) ->
-      let prec = prec_of_ast pr in
-      List.map (rule_of_ast whatfor prec) rl
-  | ast -> invalid_arg_loc (Ast.loc ast,"Metasyntax.level_of_ast")
-
-let interp_syntax_entry univ sel =
-  { sc_univ = univ;
-    sc_entries = List.flatten (List.map (level_of_ast univ) sel)}
-
-
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 34afd2200d..f15ac3d78f 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -19,7 +19,7 @@ open Unix
 (* 1. Core objects *)
 let ocamlobjs = ["unix.cma"]
 let dynobjs = ["dynlink.cma"]
-let camlp4objs = ["gramlib.cma"]
+let camlp4objs = [(*"odyl.cma"; "camlp4.cma";*) "gramlib.cma"]
 let configobjs = ["coq_config.cmo"]
 let libobjs = ocamlobjs @ camlp4objs @ configobjs
 
@@ -34,6 +34,7 @@ let parsing = split_cmo Tolink.parsing
 let proofs = split_cmo Tolink.proofs
 let tactics = split_cmo Tolink.tactics
 let toplevel = split_cmo Tolink.toplevel
+let highparsing = split_cmo Tolink.highparsing
 
 let core_objs = 
   libobjs @ lib @ kernel @ library @ pretyping @ parsing @ 
@@ -44,8 +45,7 @@ let coqsearch = ["version_searchisos.cmo"; "cmd_searchisos_line.cmo"]
 
 (* 4. Toplevel objects *)
 let camlp4objs =
-  ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo";
-   "q_coqast.cmo" ]
+  ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"; "q_util.cmo"; "q_coqast.cmo" ]
 let topobjs = camlp4objs
 
 let gramobjs = []
@@ -92,8 +92,8 @@ let files_to_link userfiles =
   let command_objs = if !searchisos then coqsearch else [] in
   let toplevel_objs = if !top then topobjs else if !opt then notopobjs else []
   in
-  let objs = core_objs @ dyn_objs @ toplevel @ command_objs @ hightactics @
-    toplevel_objs in
+  let objs = core_objs @ dyn_objs @ toplevel @ highparsing @ 
+    command_objs @ hightactics @ toplevel_objs in
   let tolink =
     if !opt then 
       (List.map native_suffix objs) @ userfiles
diff --git a/states/MakeInitial.v b/states/MakeInitial.v
index 3997ae3212..02235e1b8a 100644
--- a/states/MakeInitial.v
+++ b/states/MakeInitial.v
@@ -8,11 +8,3 @@
 Require Export Prelude.
 Require Export Logic_Type.
 Require Export Logic_TypeSyntax.
-Require Export Equality.
-Require Export Tauto.
-Require Export Inv.
-Require Export EAuto.
-Require Export AutoRewrite.
-Require Export Refine.
-Require Export EqDecide.
-Require Export Extraction.
diff --git a/syntax/MakeBare.v b/syntax/MakeBare.v
index 17a5e04a64..0ab1ac6bb6 100644
--- a/syntax/MakeBare.v
+++ b/syntax/MakeBare.v
@@ -7,4 +7,3 @@
 (***********************************************************************)
 Load PPConstr.
 Load PPCases.
-Load PPTactic.
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
deleted file mode 100644
index 4675f9c8a3..0000000000
--- a/tactics/tacentries.ml
+++ /dev/null
@@ -1,58 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-open Proof_trees
-open Tacmach
-open Tactics
-open Tacticals
-
-let v_absurd        = hide_tactic "Absurd"        dyn_absurd
-let v_contradiction = hide_tactic "Contradiction" dyn_contradiction
-let v_reflexivity   = hide_tactic "Reflexivity"   dyn_reflexivity
-let v_symmetry      = hide_tactic "Symmetry"      dyn_symmetry
-let v_transitivity  = hide_tactic "Transitivity"  dyn_transitivity
-let v_intro         = hide_tactic "Intro"         dyn_intro
-let v_intro_move    = hide_tactic "IntroMove"     dyn_intro_move
-let v_introsUntil   = hide_tactic "IntrosUntil"   dyn_intros_until
-let v_assumption    = hide_tactic "Assumption"    dyn_assumption
-let v_exact         = hide_tactic "Exact"         dyn_exact_check
-let v_reduce        = hide_tactic "Reduce"        dyn_reduce
-let v_change        = hide_tactic "Change"        dyn_change
-let v_constructor   = hide_tactic "Constructor"   dyn_constructor
-let v_left          = hide_tactic "Left"          dyn_left
-let v_right         = hide_tactic "Right"         dyn_right
-let v_split         = hide_tactic "Split"         dyn_split
-let v_clear         = hide_tactic "Clear"         dyn_clear
-let v_clear_body    = hide_tactic "ClearBody"     dyn_clear_body
-let v_move          = hide_tactic "Move"          dyn_move
-let v_move_dep      = hide_tactic "MoveDep"       dyn_move_dep
-let v_rename        = hide_tactic "Rename"        dyn_rename
-let v_apply         = hide_tactic "Apply"         dyn_apply
-let v_cutAndResolve = hide_tactic "CutAndApply"   dyn_cut_and_apply
-let v_cut           = hide_tactic "Cut"           dyn_cut
-let v_truecut       = hide_tactic "TrueCut"       dyn_true_cut
-let v_lettac        = hide_tactic "LetTac"        dyn_lettac
-let v_forward       = hide_tactic "Forward"       dyn_forward
-let v_generalize    = hide_tactic "Generalize"    dyn_generalize
-let v_generalize_dep = hide_tactic "GeneralizeDep" dyn_generalize_dep
-let v_specialize    = hide_tactic "Specialize"    dyn_new_hyp
-let v_elim          = hide_tactic "Elim"          dyn_elim
-let v_elimType      = hide_tactic "ElimType"      dyn_elim_type
-let v_induction     = hide_tactic "Induction"     dyn_old_induct
-let v_new_induction = hide_tactic "NewInduction"  dyn_new_induct
-let v_case          = hide_tactic "Case"          dyn_case
-let v_caseType      = hide_tactic "CaseType"      dyn_case_type
-let v_destruct      = hide_tactic "Destruct"      dyn_destruct
-let v_new_destruct  = hide_tactic "NewDestruct"   dyn_new_destruct
-let v_fix           = hide_tactic "Fix"           dyn_mutual_fix
-let v_cofix         = hide_tactic "Cofix"         dyn_mutual_cofix
-let vernac_instantiate =
-  hide_tactic "Instantiate" Evar_refiner.instantiate_tac
-
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
deleted file mode 100644
index 86ab39dfff..0000000000
--- a/tactics/tacentries.mli
+++ /dev/null
@@ -1,55 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Proof_type
-open Tacmach
-(*i*)
-
-(* Registered tactics. *)
-
-val v_absurd        : tactic_arg list -> tactic
-val v_contradiction : tactic_arg list -> tactic
-val v_reflexivity   : tactic_arg list -> tactic
-val v_symmetry      : tactic_arg list -> tactic
-val v_transitivity  : tactic_arg list -> tactic
-val v_intro         : tactic_arg list -> tactic
-val v_introsUntil   : tactic_arg list -> tactic
-(*i val v_tclIDTAC      : tactic_arg list -> tactic i*)
-val v_assumption    : tactic_arg list -> tactic
-val v_exact         : tactic_arg list -> tactic
-val v_reduce        : tactic_arg list -> tactic
-val v_constructor   : tactic_arg list -> tactic
-val v_left          : tactic_arg list -> tactic
-val v_right         : tactic_arg list -> tactic
-val v_split         : tactic_arg list -> tactic
-val v_clear         : tactic_arg list -> tactic
-val v_clear_body    : tactic_arg list -> tactic
-val v_move          : tactic_arg list -> tactic
-val v_move_dep      : tactic_arg list -> tactic
-val v_apply         : tactic_arg list -> tactic
-val v_cutAndResolve : tactic_arg list -> tactic
-val v_cut           : tactic_arg list -> tactic
-val v_truecut       : tactic_arg list -> tactic
-val v_lettac        : tactic_arg list -> tactic
-val v_generalize    : tactic_arg list -> tactic
-val v_generalize_dep : tactic_arg list -> tactic
-val v_specialize    : tactic_arg list -> tactic
-val v_elim          : tactic_arg list -> tactic
-val v_elimType      : tactic_arg list -> tactic
-val v_induction     : tactic_arg list -> tactic
-(*i val v_new_induction : tactic_arg list -> tactic i*)
-val v_case          : tactic_arg list -> tactic
-val v_caseType      : tactic_arg list -> tactic
-val v_destruct      : tactic_arg list -> tactic
-(*i val v_new_destruct  : tactic_arg list -> tactic i*)
-val v_fix           : tactic_arg list -> tactic
-val v_cofix         : tactic_arg list -> tactic
-val vernac_instantiate : tactic_arg list -> tactic
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 99342140e4..042a18738a 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -128,8 +128,8 @@ let standard sds =
 let implicit () =
   let ml_rules () =
     print ".mli.cmi:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
+    print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+    print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
   and v_rule () =
     print ".v.vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
     print ".v.vi:\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
@@ -182,6 +182,10 @@ let variables l =
   print "CAMLOPTLINK=ocamlopt\n";
   print "COQDEP=$(COQBIN)coqdep -c\n";
   print "COQVO2XML=coq_vo2xml\n";
+  print "GRAMMARS=grammar.cma g_constr.cmo g_tactic.cmo g_ltac.cmo \\
+  g_basevernac.cmo tacextend.cmo vernacextend.cmo\n";
+  print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n";
+  print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
   var_aux l;
   print "\n"