changes in declarative language : by term using tactic

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

6 files changed, 374 insertions, 321 deletions

diff --git a/.depend b/.depend
index 287e706e5..7866da407 100644
--- a/.depend
+++ b/.depend
@@ -54,12 +54,12 @@ kernel/indtypes.cmi: kernel/univ.cmi kernel/typeops.cmi kernel/term.cmi \
     kernel/declarations.cmi 
 kernel/inductive.cmi: kernel/univ.cmi kernel/term.cmi kernel/sign.cmi \
     kernel/names.cmi kernel/environ.cmi kernel/declarations.cmi 
-kernel/modops.cmi: lib/util.cmi kernel/univ.cmi kernel/names.cmi \
-    kernel/mod_subst.cmi kernel/environ.cmi kernel/entries.cmi \
-    kernel/declarations.cmi 
 kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi 
 kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \
     kernel/declarations.cmi 
+kernel/modops.cmi: lib/util.cmi kernel/univ.cmi kernel/names.cmi \
+    kernel/mod_subst.cmi kernel/environ.cmi kernel/entries.cmi \
+    kernel/declarations.cmi 
 kernel/names.cmi: lib/predicate.cmi lib/pp.cmi 
 kernel/pre_env.cmi: lib/util.cmi kernel/univ.cmi kernel/term.cmi \
     kernel/sign.cmi kernel/names.cmi kernel/declarations.cmi 
@@ -86,6 +86,9 @@ kernel/vm.cmi: kernel/term.cmi kernel/names.cmi kernel/cemitcodes.cmi \
     kernel/cbytecodes.cmi 
 lib/bigint.cmi: lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
+lib/rtree.cmi: lib/pp.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi lib/compat.cmo 
 library/declare.cmi: kernel/term.cmi kernel/sign.cmi kernel/safe_typing.cmi \
     library/nametab.cmi kernel/names.cmi library/libnames.cmi \
     kernel/indtypes.cmi kernel/environ.cmi kernel/entries.cmi \
@@ -104,9 +107,9 @@ library/goptions.cmi: lib/util.cmi kernel/term.cmi lib/pp.cmi \
     library/libnames.cmi 
 library/impargs.cmi: interp/topconstr.cmi kernel/term.cmi library/nametab.cmi \
     kernel/names.cmi library/libnames.cmi kernel/environ.cmi 
-library/lib.cmi: lib/util.cmi kernel/term.cmi library/summary.cmi \
-    kernel/sign.cmi kernel/names.cmi kernel/mod_subst.cmi \
-    library/libobject.cmi library/libnames.cmi 
+library/lib.cmi: lib/util.cmi library/summary.cmi kernel/sign.cmi \
+    kernel/names.cmi kernel/mod_subst.cmi library/libobject.cmi \
+    library/libnames.cmi 
 library/libnames.cmi: lib/util.cmi kernel/term.cmi lib/predicate.cmi \
     lib/pp.cmi kernel/names.cmi kernel/mod_subst.cmi 
 library/libobject.cmi: kernel/names.cmi kernel/mod_subst.cmi \
@@ -116,9 +119,6 @@ library/library.cmi: lib/util.cmi lib/system.cmi lib/pp.cmi kernel/names.cmi \
 library/nameops.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi 
 library/nametab.cmi: lib/util.cmi lib/pp.cmi kernel/names.cmi \
     library/libnames.cmi 
-lib/rtree.cmi: lib/pp.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi lib/compat.cmo 
 parsing/egrammar.cmi: toplevel/vernacexpr.cmo lib/util.cmi \
     interp/topconstr.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \
     interp/ppextend.cmi parsing/pcoq.cmi kernel/names.cmi \
@@ -368,12 +368,12 @@ toplevel/record.cmi: toplevel/vernacexpr.cmo interp/topconstr.cmi \
 toplevel/searchisos.cmi: kernel/term.cmi kernel/names.cmi \
     library/libobject.cmi 
 toplevel/toplevel.cmi: lib/pp.cmi parsing/pcoq.cmi 
+toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi 
 toplevel/vernacentries.cmi: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
     lib/util.cmi interp/topconstr.cmi kernel/term.cmi \
     pretyping/reductionops.cmi kernel/names.cmi library/libnames.cmi \
     pretyping/evd.cmi kernel/environ.cmi 
 toplevel/vernacinterp.cmi: proofs/tacexpr.cmo 
-toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi 
 toplevel/whelp.cmi: interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \
     kernel/environ.cmi 
 contrib/cc/ccalgo.cmi: lib/util.cmi kernel/term.cmi lib/pp.cmi \
@@ -383,9 +383,9 @@ contrib/cc/ccproof.cmi: kernel/term.cmi kernel/names.cmi \
 contrib/cc/cctac.cmi: kernel/term.cmi proofs/proof_type.cmi 
 contrib/correctness/past.cmi: lib/util.cmi interp/topconstr.cmi \
     kernel/term.cmi kernel/names.cmi 
+contrib/correctness/pcic.cmi: pretyping/rawterm.cmi 
 contrib/correctness/pcicenv.cmi: kernel/term.cmi kernel/sign.cmi \
     kernel/names.cmi 
-contrib/correctness/pcic.cmi: pretyping/rawterm.cmi 
 contrib/correctness/pdb.cmi: kernel/names.cmi 
 contrib/correctness/peffect.cmi: lib/pp.cmi kernel/names.cmi 
 contrib/correctness/penv.cmi: kernel/term.cmi kernel/names.cmi \
@@ -453,10 +453,10 @@ contrib/funind/functional_principles_types.cmi: kernel/term.cmi \
 contrib/funind/indfun_common.cmi: kernel/term.cmi proofs/tacexpr.cmo \
     pretyping/rawterm.cmi lib/pp.cmi kernel/names.cmi library/libnames.cmi \
     kernel/entries.cmi library/decl_kinds.cmo 
-contrib/funind/rawtermops.cmi: lib/util.cmi pretyping/rawterm.cmi \
-    kernel/names.cmi library/libnames.cmi 
 contrib/funind/rawterm_to_relation.cmi: interp/topconstr.cmi \
     pretyping/rawterm.cmi kernel/names.cmi 
+contrib/funind/rawtermops.cmi: lib/util.cmi pretyping/rawterm.cmi \
+    kernel/names.cmi library/libnames.cmi 
 contrib/funind/tacinvutils.cmi: lib/util.cmi pretyping/termops.cmi \
     kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
     proofs/tacmach.cmi tactics/tacinterp.cmi tactics/refine.cmi \
@@ -493,6 +493,7 @@ contrib/rtauto/refl_tauto.cmi: kernel/term.cmi proofs/tacmach.cmi \
 contrib/subtac/context.cmi: kernel/term.cmi kernel/names.cmi 
 contrib/subtac/eterm.cmi: lib/util.cmi kernel/term.cmi proofs/tacmach.cmi \
     kernel/names.cmi pretyping/evd.cmi 
+contrib/subtac/subtac.cmi: toplevel/vernacexpr.cmo lib/util.cmi 
 contrib/subtac/subtac_cases.cmi: lib/util.cmi kernel/term.cmi \
     pretyping/rawterm.cmi kernel/names.cmi pretyping/inductiveops.cmi \
     pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \
@@ -505,7 +506,6 @@ contrib/subtac/subtac_command.cmi: toplevel/vernacexpr.cmo \
 contrib/subtac/subtac_errors.cmi: lib/util.cmi lib/pp.cmi 
 contrib/subtac/subtac_interp_fixpoint.cmi: lib/util.cmi interp/topconstr.cmi \
     lib/pp.cmi kernel/names.cmi library/libnames.cmi 
-contrib/subtac/subtac.cmi: toplevel/vernacexpr.cmo lib/util.cmi 
 contrib/subtac/subtac_obligations.cmi: lib/util.cmi interp/topconstr.cmi \
     kernel/term.cmi proofs/proof_type.cmi kernel/names.cmi 
 contrib/subtac/subtac_pretyping.cmi: interp/topconstr.cmi kernel/term.cmi \
@@ -533,9 +533,10 @@ dev/top_printers.cmo: toplevel/vernacinterp.cmi lib/util.cmi kernel/univ.cmi \
     pretyping/termops.cmi kernel/term.cmi parsing/tactic_printer.cmi \
     lib/system.cmi kernel/sign.cmi proofs/refiner.cmi proofs/proof_trees.cmi \
     parsing/printer.cmi parsing/pptactic.cmi lib/pp.cmi proofs/pfedit.cmi \
-    parsing/pcoq.cmi kernel/names.cmi library/nameops.cmi proofs/logic.cmi \
-    library/libobject.cmi library/libnames.cmi library/goptions.cmi \
-    library/global.cmi interp/genarg.cmi pretyping/evd.cmi kernel/environ.cmi \
+    parsing/pcoq.cmi kernel/names.cmi library/nameops.cmi \
+    kernel/mod_subst.cmi proofs/logic.cmi library/libobject.cmi \
+    library/libnames.cmi library/goptions.cmi library/global.cmi \
+    interp/genarg.cmi pretyping/evd.cmi kernel/environ.cmi \
     parsing/egrammar.cmi kernel/declarations.cmi interp/constrintern.cmi \
     interp/constrextern.cmi kernel/closure.cmi pretyping/clenv.cmi \
     toplevel/cerrors.cmi lib/bigint.cmi 
@@ -543,9 +544,10 @@ dev/top_printers.cmx: toplevel/vernacinterp.cmx lib/util.cmx kernel/univ.cmx \
     pretyping/termops.cmx kernel/term.cmx parsing/tactic_printer.cmx \
     lib/system.cmx kernel/sign.cmx proofs/refiner.cmx proofs/proof_trees.cmx \
     parsing/printer.cmx parsing/pptactic.cmx lib/pp.cmx proofs/pfedit.cmx \
-    parsing/pcoq.cmx kernel/names.cmx library/nameops.cmx proofs/logic.cmx \
-    library/libobject.cmx library/libnames.cmx library/goptions.cmx \
-    library/global.cmx interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \
+    parsing/pcoq.cmx kernel/names.cmx library/nameops.cmx \
+    kernel/mod_subst.cmx proofs/logic.cmx library/libobject.cmx \
+    library/libnames.cmx library/goptions.cmx library/global.cmx \
+    interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \
     parsing/egrammar.cmx kernel/declarations.cmx interp/constrintern.cmx \
     interp/constrextern.cmx kernel/closure.cmx pretyping/clenv.cmx \
     toplevel/cerrors.cmx lib/bigint.cmx 
@@ -563,16 +565,6 @@ ide/config_lexer.cmo: lib/util.cmi ide/config_parser.cmi
 ide/config_lexer.cmx: lib/util.cmx ide/config_parser.cmx 
 ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi 
 ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi 
-ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \
-    lib/system.cmi ide/preferences.cmi lib/pp.cmi proofs/pfedit.cmi \
-    ide/ideutils.cmi ide/highlight.cmo ide/find_phrase.cmo \
-    proofs/decl_mode.cmi config/coq_config.cmi ide/coq_commands.cmo \
-    ide/coq.cmi ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi 
-ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \
-    lib/system.cmx ide/preferences.cmx lib/pp.cmx proofs/pfedit.cmx \
-    ide/ideutils.cmx ide/highlight.cmx ide/find_phrase.cmx \
-    proofs/decl_mode.cmx config/coq_config.cmx ide/coq_commands.cmx \
-    ide/coq.cmx ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi 
 ide/coq.cmo: toplevel/vernacexpr.cmo toplevel/vernacentries.cmi \
     toplevel/vernac.cmi lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
     proofs/tacmach.cmi tactics/tacinterp.cmi lib/system.cmi \
@@ -597,6 +589,16 @@ ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \
     config/coq_config.cmx toplevel/cerrors.cmx ide/coq.cmi 
 ide/coq_tactics.cmo: ide/coq_tactics.cmi 
 ide/coq_tactics.cmx: ide/coq_tactics.cmi 
+ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \
+    lib/system.cmi ide/preferences.cmi lib/pp.cmi proofs/pfedit.cmi \
+    ide/ideutils.cmi ide/highlight.cmo ide/find_phrase.cmo \
+    proofs/decl_mode.cmi config/coq_config.cmi ide/coq_commands.cmo \
+    ide/coq.cmi ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi 
+ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \
+    lib/system.cmx ide/preferences.cmx lib/pp.cmx proofs/pfedit.cmx \
+    ide/ideutils.cmx ide/highlight.cmx ide/find_phrase.cmx \
+    proofs/decl_mode.cmx config/coq_config.cmx ide/coq_commands.cmx \
+    ide/coq.cmx ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi 
 ide/find_phrase.cmo: ide/preferences.cmi ide/ideutils.cmi 
 ide/find_phrase.cmx: ide/preferences.cmx ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmi 
@@ -781,14 +783,6 @@ kernel/inductive.cmx: lib/util.cmx kernel/univ.cmx kernel/type_errors.cmx \
     kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx kernel/names.cmx \
     kernel/environ.cmx kernel/declarations.cmx kernel/closure.cmx \
     kernel/inductive.cmi 
-kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \
-    kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \
-    kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \
-    kernel/modops.cmi 
-kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \
-    kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \
-    kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \
-    kernel/modops.cmi 
 kernel/mod_subst.cmo: lib/util.cmi kernel/term.cmi lib/pp.cmi \
     kernel/names.cmi kernel/mod_subst.cmi 
 kernel/mod_subst.cmx: lib/util.cmx kernel/term.cmx lib/pp.cmx \
@@ -803,6 +797,14 @@ kernel/mod_typing.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \
     kernel/names.cmx kernel/modops.cmx kernel/mod_subst.cmx \
     kernel/environ.cmx kernel/entries.cmx kernel/declarations.cmx \
     kernel/cemitcodes.cmx kernel/mod_typing.cmi 
+kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \
+    kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \
+    kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \
+    kernel/modops.cmi 
+kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \
+    kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \
+    kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \
+    kernel/modops.cmi 
 kernel/names.cmo: lib/util.cmi lib/predicate.cmi lib/pp.cmi lib/hashcons.cmi \
     kernel/names.cmi 
 kernel/names.cmx: lib/util.cmx lib/predicate.cmx lib/pp.cmx lib/hashcons.cmx \
@@ -840,13 +842,15 @@ kernel/sign.cmo: lib/util.cmi kernel/term.cmi kernel/names.cmi \
 kernel/sign.cmx: lib/util.cmx kernel/term.cmx kernel/names.cmx \
     kernel/sign.cmi 
 kernel/subtyping.cmo: lib/util.cmi kernel/univ.cmi kernel/typeops.cmi \
-    kernel/term.cmi kernel/reduction.cmi kernel/names.cmi kernel/modops.cmi \
-    kernel/mod_subst.cmi kernel/inductive.cmi kernel/environ.cmi \
-    kernel/entries.cmi kernel/declarations.cmi kernel/subtyping.cmi 
+    kernel/term.cmi kernel/sign.cmi kernel/reduction.cmi kernel/names.cmi \
+    kernel/modops.cmi kernel/mod_subst.cmi kernel/inductive.cmi \
+    kernel/environ.cmi kernel/entries.cmi kernel/declarations.cmi \
+    kernel/subtyping.cmi 
 kernel/subtyping.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \
-    kernel/term.cmx kernel/reduction.cmx kernel/names.cmx kernel/modops.cmx \
-    kernel/mod_subst.cmx kernel/inductive.cmx kernel/environ.cmx \
-    kernel/entries.cmx kernel/declarations.cmx kernel/subtyping.cmi 
+    kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx kernel/names.cmx \
+    kernel/modops.cmx kernel/mod_subst.cmx kernel/inductive.cmx \
+    kernel/environ.cmx kernel/entries.cmx kernel/declarations.cmx \
+    kernel/subtyping.cmi 
 kernel/term.cmo: lib/util.cmi kernel/univ.cmi lib/pp.cmi kernel/names.cmi \
     lib/hashcons.cmi kernel/esubst.cmi kernel/term.cmi 
 kernel/term.cmx: lib/util.cmx kernel/univ.cmx lib/pp.cmx kernel/names.cmx \
@@ -901,10 +905,10 @@ lib/edit.cmo: lib/util.cmi lib/pp.cmi lib/bstack.cmi lib/edit.cmi
 lib/edit.cmx: lib/util.cmx lib/pp.cmx lib/bstack.cmx lib/edit.cmi 
 lib/explore.cmo: lib/explore.cmi 
 lib/explore.cmx: lib/explore.cmi 
-lib/gmapl.cmo: lib/util.cmi lib/gmap.cmi lib/gmapl.cmi 
-lib/gmapl.cmx: lib/util.cmx lib/gmap.cmx lib/gmapl.cmi 
 lib/gmap.cmo: lib/gmap.cmi 
 lib/gmap.cmx: lib/gmap.cmi 
+lib/gmapl.cmo: lib/util.cmi lib/gmap.cmi lib/gmapl.cmi 
+lib/gmapl.cmx: lib/util.cmx lib/gmap.cmx lib/gmapl.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
@@ -913,14 +917,24 @@ lib/heap.cmo: lib/heap.cmi
 lib/heap.cmx: lib/heap.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
-lib/pp_control.cmo: lib/pp_control.cmi 
-lib/pp_control.cmx: lib/pp_control.cmi 
 lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
 lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
+lib/pp_control.cmo: lib/pp_control.cmi 
+lib/pp_control.cmx: lib/pp_control.cmi 
 lib/predicate.cmo: lib/predicate.cmi 
 lib/predicate.cmx: lib/predicate.cmi 
 lib/profile.cmo: lib/profile.cmi 
 lib/profile.cmx: lib/profile.cmi 
+lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi 
+lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi 
+lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi 
+lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi 
+library/decl_kinds.cmo: lib/util.cmi 
+library/decl_kinds.cmx: lib/util.cmx 
 library/declare.cmo: lib/util.cmi kernel/univ.cmi kernel/typeops.cmi \
     kernel/type_errors.cmi kernel/term.cmi library/summary.cmi \
     kernel/sign.cmi kernel/safe_typing.cmi kernel/reduction.cmi lib/pp.cmi \
@@ -953,8 +967,6 @@ library/declaremods.cmx: lib/util.cmx library/summary.cmx \
     library/libobject.cmx library/libnames.cmx library/lib.cmx \
     library/global.cmx kernel/environ.cmx kernel/entries.cmx \
     kernel/declarations.cmx library/declaremods.cmi 
-library/decl_kinds.cmo: lib/util.cmi 
-library/decl_kinds.cmx: lib/util.cmx 
 library/dischargedhypsmap.cmo: lib/util.cmi kernel/term.cmi \
     library/summary.cmi kernel/reduction.cmi library/nametab.cmi \
     kernel/names.cmi library/libobject.cmi library/libnames.cmi \
@@ -1037,14 +1049,6 @@ library/states.cmx: lib/system.cmx library/summary.cmx library/library.cmx \
     library/lib.cmx library/states.cmi 
 library/summary.cmo: lib/util.cmi lib/pp.cmi lib/dyn.cmi library/summary.cmi 
 library/summary.cmx: lib/util.cmx lib/pp.cmx lib/dyn.cmx library/summary.cmi 
-lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi 
-lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi 
-lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi 
-lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi 
 parsing/argextend.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     parsing/q_util.cmi parsing/q_coqast.cmo parsing/pcoq.cmi \
     interp/genarg.cmi 
@@ -1725,17 +1729,17 @@ proofs/tacexpr.cmx: lib/util.cmx interp/topconstr.cmx kernel/term.cmx \
     library/decl_kinds.cmx 
 proofs/tacmach.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \
     kernel/term.cmi pretyping/tacred.cmi proofs/tacexpr.cmo kernel/sign.cmi \
-    proofs/refiner.cmi pretyping/reductionops.cmi proofs/redexpr.cmi \
-    pretyping/rawterm.cmi proofs/proof_type.cmi proofs/proof_trees.cmi \
-    lib/pp.cmi kernel/names.cmi library/nameops.cmi proofs/logic.cmi \
-    library/global.cmi pretyping/evd.cmi kernel/environ.cmi \
+    pretyping/retyping.cmi proofs/refiner.cmi pretyping/reductionops.cmi \
+    proofs/redexpr.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \
+    proofs/proof_trees.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \
+    proofs/logic.cmi library/global.cmi pretyping/evd.cmi kernel/environ.cmi \
     interp/constrintern.cmi proofs/tacmach.cmi 
 proofs/tacmach.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \
     kernel/term.cmx pretyping/tacred.cmx proofs/tacexpr.cmx kernel/sign.cmx \
-    proofs/refiner.cmx pretyping/reductionops.cmx proofs/redexpr.cmx \
-    pretyping/rawterm.cmx proofs/proof_type.cmx proofs/proof_trees.cmx \
-    lib/pp.cmx kernel/names.cmx library/nameops.cmx proofs/logic.cmx \
-    library/global.cmx pretyping/evd.cmx kernel/environ.cmx \
+    pretyping/retyping.cmx proofs/refiner.cmx pretyping/reductionops.cmx \
+    proofs/redexpr.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \
+    proofs/proof_trees.cmx lib/pp.cmx kernel/names.cmx library/nameops.cmx \
+    proofs/logic.cmx library/global.cmx pretyping/evd.cmx kernel/environ.cmx \
     interp/constrintern.cmx proofs/tacmach.cmi 
 proofs/tactic_debug.cmo: pretyping/termops.cmi proofs/tacexpr.cmo \
     proofs/refiner.cmi proofs/proof_trees.cmi lib/pp.cmi kernel/names.cmi \
@@ -1826,29 +1830,29 @@ tactics/decl_interp.cmx: lib/util.cmx interp/topconstr.cmx \
     proofs/decl_expr.cmi interp/coqlib.cmx interp/constrintern.cmx \
     kernel/closure.cmx tactics/decl_interp.cmi 
 tactics/decl_proof_instr.cmo: lib/util.cmi pretyping/unification.cmi \
-    pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \
-    tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \
-    proofs/tacexpr.cmo proofs/refiner.cmi pretyping/reductionops.cmi \
-    kernel/reduction.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \
-    proofs/proof_trees.cmi parsing/printer.cmi lib/pp.cmi proofs/pfedit.cmi \
-    kernel/names.cmi library/nameops.cmi library/libnames.cmi \
-    pretyping/inductiveops.cmi kernel/inductive.cmi library/goptions.cmi \
-    library/global.cmi interp/genarg.cmi pretyping/evd.cmi kernel/environ.cmi \
-    kernel/declarations.cmi proofs/decl_mode.cmi tactics/decl_interp.cmi \
-    proofs/decl_expr.cmi interp/coqlib.cmi kernel/closure.cmi \
-    tactics/decl_proof_instr.cmi 
+    kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \
+    tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \
+    tactics/tacinterp.cmi proofs/tacexpr.cmo proofs/refiner.cmi \
+    pretyping/reductionops.cmi kernel/reduction.cmi pretyping/rawterm.cmi \
+    proofs/proof_type.cmi proofs/proof_trees.cmi parsing/printer.cmi \
+    lib/pp.cmi proofs/pfedit.cmi kernel/names.cmi library/nameops.cmi \
+    library/libnames.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \
+    library/goptions.cmi library/global.cmi interp/genarg.cmi \
+    pretyping/evd.cmi kernel/environ.cmi kernel/declarations.cmi \
+    proofs/decl_mode.cmi tactics/decl_interp.cmi proofs/decl_expr.cmi \
+    interp/coqlib.cmi kernel/closure.cmi tactics/decl_proof_instr.cmi 
 tactics/decl_proof_instr.cmx: lib/util.cmx pretyping/unification.cmx \
-    pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \
-    tactics/tacticals.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \
-    proofs/tacexpr.cmx proofs/refiner.cmx pretyping/reductionops.cmx \
-    kernel/reduction.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \
-    proofs/proof_trees.cmx parsing/printer.cmx lib/pp.cmx proofs/pfedit.cmx \
-    kernel/names.cmx library/nameops.cmx library/libnames.cmx \
-    pretyping/inductiveops.cmx kernel/inductive.cmx library/goptions.cmx \
-    library/global.cmx interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \
-    kernel/declarations.cmx proofs/decl_mode.cmx tactics/decl_interp.cmx \
-    proofs/decl_expr.cmi interp/coqlib.cmx kernel/closure.cmx \
-    tactics/decl_proof_instr.cmi 
+    kernel/type_errors.cmx pretyping/termops.cmx kernel/term.cmx \
+    tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \
+    tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/refiner.cmx \
+    pretyping/reductionops.cmx kernel/reduction.cmx pretyping/rawterm.cmx \
+    proofs/proof_type.cmx proofs/proof_trees.cmx parsing/printer.cmx \
+    lib/pp.cmx proofs/pfedit.cmx kernel/names.cmx library/nameops.cmx \
+    library/libnames.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \
+    library/goptions.cmx library/global.cmx interp/genarg.cmx \
+    pretyping/evd.cmx kernel/environ.cmx kernel/declarations.cmx \
+    proofs/decl_mode.cmx tactics/decl_interp.cmx proofs/decl_expr.cmi \
+    interp/coqlib.cmx kernel/closure.cmx tactics/decl_proof_instr.cmi 
 tactics/dhyp.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \
     tactics/tacticals.cmi proofs/tacmach.cmi proofs/tacexpr.cmo \
     library/summary.cmi proofs/refiner.cmi kernel/reduction.cmi \
@@ -2215,8 +2219,6 @@ tactics/termdn.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \
     pretyping/pattern.cmx library/nametab.cmx kernel/names.cmx \
     library/nameops.cmx library/libnames.cmx tactics/dn.cmx \
     tactics/termdn.cmi 
-test-suite/zarith.cmo: test-suite/zarith.cmi 
-test-suite/zarith.cmx: test-suite/zarith.cmi 
 tools/coqdep.cmo: tools/coqdep_lexer.cmo config/coq_config.cmi 
 tools/coqdep.cmx: tools/coqdep_lexer.cmx config/coq_config.cmx 
 tools/gallina.cmo: tools/gallina_lexer.cmo 
@@ -2409,6 +2411,16 @@ toplevel/toplevel.cmx: toplevel/vernacexpr.cmx toplevel/vernac.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/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacentries.cmi lib/util.cmi lib/system.cmi library/states.cmi \
+    parsing/ppvernac.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \
+    lib/options.cmi kernel/names.cmi library/library.cmi library/lib.cmi \
+    parsing/lexer.cmi interp/constrintern.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacentries.cmx lib/util.cmx lib/system.cmx library/states.cmx \
+    parsing/ppvernac.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \
+    lib/options.cmx kernel/names.cmx library/library.cmx library/lib.cmx \
+    parsing/lexer.cmx interp/constrintern.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: kernel/vm.cmi toplevel/vernacinterp.cmi \
     toplevel/vernacexpr.cmo kernel/vconv.cmi lib/util.cmi kernel/univ.cmi \
     kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \
@@ -2473,16 +2485,6 @@ toplevel/vernacinterp.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/proof_type.cmx lib/pp.cmx \
     lib/options.cmx kernel/names.cmx library/libnames.cmx toplevel/himsg.cmx \
     toplevel/vernacinterp.cmi 
-toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
-    toplevel/vernacentries.cmi lib/util.cmi lib/system.cmi library/states.cmi \
-    parsing/ppvernac.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \
-    lib/options.cmi kernel/names.cmi library/library.cmi library/lib.cmi \
-    parsing/lexer.cmi interp/constrintern.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \
-    toplevel/vernacentries.cmx lib/util.cmx lib/system.cmx library/states.cmx \
-    parsing/ppvernac.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \
-    lib/options.cmx kernel/names.cmx library/library.cmx library/lib.cmx \
-    parsing/lexer.cmx interp/constrintern.cmx toplevel/vernac.cmi 
 toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi lib/system.cmi \
     interp/syntax_def.cmi proofs/refiner.cmi pretyping/rawterm.cmi lib/pp.cmi \
@@ -2531,12 +2533,6 @@ contrib/cc/g_congruence.cmx: lib/util.cmx tactics/tactics.cmx \
     tactics/tacticals.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
     parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx interp/genarg.cmx \
     parsing/egrammar.cmx toplevel/cerrors.cmx contrib/cc/cctac.cmx 
-contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \
-    kernel/sign.cmi kernel/names.cmi library/global.cmi \
-    contrib/correctness/pcicenv.cmi 
-contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \
-    kernel/sign.cmx kernel/names.cmx library/global.cmx \
-    contrib/correctness/pcicenv.cmi 
 contrib/correctness/pcic.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \
     kernel/term.cmi kernel/sign.cmi toplevel/record.cmi pretyping/rawterm.cmi \
@@ -2551,6 +2547,12 @@ contrib/correctness/pcic.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     library/libnames.cmx kernel/indtypes.cmx library/global.cmx \
     kernel/entries.cmx pretyping/detyping.cmx library/declare.cmx \
     kernel/declarations.cmx contrib/correctness/pcic.cmi 
+contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \
+    kernel/sign.cmi kernel/names.cmi library/global.cmi \
+    contrib/correctness/pcicenv.cmi 
+contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \
+    kernel/sign.cmx kernel/names.cmx library/global.cmx \
+    contrib/correctness/pcicenv.cmi 
 contrib/correctness/pdb.cmo: pretyping/termops.cmi kernel/term.cmi \
     library/nametab.cmi kernel/names.cmi library/global.cmi \
     interp/constrintern.cmi contrib/correctness/pdb.cmi 
@@ -3023,6 +3025,38 @@ contrib/funind/functional_principles_types.cmx: lib/util.cmx \
     kernel/environ.cmx kernel/entries.cmx library/declare.cmx \
     kernel/declarations.cmx library/decl_kinds.cmx toplevel/command.cmx \
     kernel/closure.cmx contrib/funind/functional_principles_types.cmi 
+contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
+    kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \
+    kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
+    proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
+    library/states.cmi kernel/sign.cmi contrib/recdef/recdef.cmo \
+    contrib/funind/rawterm_to_relation.cmi pretyping/rawterm.cmi \
+    parsing/printer.cmi parsing/ppconstr.cmi lib/pp.cmi lib/options.cmi \
+    interp/notation.cmi kernel/names.cmi library/nameops.cmi \
+    library/libnames.cmi contrib/funind/invfun.cmo pretyping/indrec.cmi \
+    contrib/funind/indfun_common.cmi library/impargs.cmi \
+    tactics/hiddentac.cmi library/global.cmi \
+    contrib/funind/functional_principles_types.cmi \
+    contrib/funind/functional_principles_proofs.cmi pretyping/evd.cmi \
+    tactics/equality.cmi kernel/environ.cmi kernel/declarations.cmi \
+    library/decl_kinds.cmo interp/constrintern.cmi interp/constrextern.cmi \
+    toplevel/command.cmi toplevel/cerrors.cmi 
+contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
+    kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \
+    kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \
+    proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
+    library/states.cmx kernel/sign.cmx contrib/recdef/recdef.cmx \
+    contrib/funind/rawterm_to_relation.cmx pretyping/rawterm.cmx \
+    parsing/printer.cmx parsing/ppconstr.cmx lib/pp.cmx lib/options.cmx \
+    interp/notation.cmx kernel/names.cmx library/nameops.cmx \
+    library/libnames.cmx contrib/funind/invfun.cmx pretyping/indrec.cmx \
+    contrib/funind/indfun_common.cmx library/impargs.cmx \
+    tactics/hiddentac.cmx library/global.cmx \
+    contrib/funind/functional_principles_types.cmx \
+    contrib/funind/functional_principles_proofs.cmx pretyping/evd.cmx \
+    tactics/equality.cmx kernel/environ.cmx kernel/declarations.cmx \
+    library/decl_kinds.cmx interp/constrintern.cmx interp/constrextern.cmx \
+    toplevel/command.cmx toplevel/cerrors.cmx 
 contrib/funind/indfun_common.cmo: lib/util.cmi pretyping/termops.cmi \
     kernel/term.cmi library/summary.cmi proofs/refiner.cmi \
     pretyping/reductionops.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \
@@ -3071,38 +3105,6 @@ contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
     contrib/funind/functional_principles_types.cmx pretyping/evd.cmx \
     parsing/egrammar.cmx interp/coqlib.cmx interp/constrintern.cmx \
     toplevel/cerrors.cmx 
-contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
-    kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \
-    kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
-    proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
-    library/states.cmi kernel/sign.cmi contrib/recdef/recdef.cmo \
-    contrib/funind/rawterm_to_relation.cmi pretyping/rawterm.cmi \
-    parsing/printer.cmi parsing/ppconstr.cmi lib/pp.cmi lib/options.cmi \
-    interp/notation.cmi kernel/names.cmi library/nameops.cmi \
-    library/libnames.cmi contrib/funind/invfun.cmo pretyping/indrec.cmi \
-    contrib/funind/indfun_common.cmi library/impargs.cmi \
-    tactics/hiddentac.cmi library/global.cmi \
-    contrib/funind/functional_principles_types.cmi \
-    contrib/funind/functional_principles_proofs.cmi pretyping/evd.cmi \
-    tactics/equality.cmi kernel/environ.cmi kernel/declarations.cmi \
-    library/decl_kinds.cmo interp/constrintern.cmi interp/constrextern.cmi \
-    toplevel/command.cmi toplevel/cerrors.cmi 
-contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
-    kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \
-    kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \
-    proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
-    library/states.cmx kernel/sign.cmx contrib/recdef/recdef.cmx \
-    contrib/funind/rawterm_to_relation.cmx pretyping/rawterm.cmx \
-    parsing/printer.cmx parsing/ppconstr.cmx lib/pp.cmx lib/options.cmx \
-    interp/notation.cmx kernel/names.cmx library/nameops.cmx \
-    library/libnames.cmx contrib/funind/invfun.cmx pretyping/indrec.cmx \
-    contrib/funind/indfun_common.cmx library/impargs.cmx \
-    tactics/hiddentac.cmx library/global.cmx \
-    contrib/funind/functional_principles_types.cmx \
-    contrib/funind/functional_principles_proofs.cmx pretyping/evd.cmx \
-    tactics/equality.cmx kernel/environ.cmx kernel/declarations.cmx \
-    library/decl_kinds.cmx interp/constrintern.cmx interp/constrextern.cmx \
-    toplevel/command.cmx toplevel/cerrors.cmx 
 contrib/funind/invfun.cmo: toplevel/vernacentries.cmi lib/util.cmi \
     pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \
     tactics/tauto.cmo tactics/tactics.cmi tactics/tacticals.cmi \
@@ -3149,16 +3151,6 @@ contrib/funind/merge.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     pretyping/evd.cmx kernel/environ.cmx pretyping/detyping.cmx \
     kernel/declarations.cmx interp/constrintern.cmx interp/constrextern.cmx \
     toplevel/command.cmx 
-contrib/funind/rawtermops.cmo: lib/util.cmi pretyping/rawterm.cmi lib/pp.cmi \
-    kernel/names.cmi library/nameops.cmi library/libnames.cmi \
-    pretyping/inductiveops.cmi contrib/funind/indfun_common.cmi \
-    library/global.cmi pretyping/evd.cmi interp/coqlib.cmi \
-    contrib/funind/rawtermops.cmi 
-contrib/funind/rawtermops.cmx: lib/util.cmx pretyping/rawterm.cmx lib/pp.cmx \
-    kernel/names.cmx library/nameops.cmx library/libnames.cmx \
-    pretyping/inductiveops.cmx contrib/funind/indfun_common.cmx \
-    library/global.cmx pretyping/evd.cmx interp/coqlib.cmx \
-    contrib/funind/rawtermops.cmi 
 contrib/funind/rawterm_to_relation.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     pretyping/typing.cmi interp/topconstr.cmi pretyping/termops.cmi \
     kernel/term.cmi tactics/tacinterp.cmi lib/system.cmi kernel/sign.cmi \
@@ -3183,6 +3175,16 @@ contrib/funind/rawterm_to_relation.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     pretyping/detyping.cmx kernel/declarations.cmx interp/coqlib.cmx \
     interp/constrextern.cmx toplevel/command.cmx toplevel/cerrors.cmx \
     contrib/funind/rawterm_to_relation.cmi 
+contrib/funind/rawtermops.cmo: lib/util.cmi pretyping/rawterm.cmi lib/pp.cmi \
+    kernel/names.cmi library/nameops.cmi library/libnames.cmi \
+    pretyping/inductiveops.cmi contrib/funind/indfun_common.cmi \
+    library/global.cmi pretyping/evd.cmi interp/coqlib.cmi \
+    contrib/funind/rawtermops.cmi 
+contrib/funind/rawtermops.cmx: lib/util.cmx pretyping/rawterm.cmx lib/pp.cmx \
+    kernel/names.cmx library/nameops.cmx library/libnames.cmx \
+    pretyping/inductiveops.cmx contrib/funind/indfun_common.cmx \
+    library/global.cmx pretyping/evd.cmx interp/coqlib.cmx \
+    contrib/funind/rawtermops.cmi 
 contrib/funind/tacinv.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \
     tactics/tactics.cmi tactics/tacticals.cmi pretyping/tacred.cmi \
@@ -3381,14 +3383,6 @@ contrib/interface/pbp.cmx: lib/util.cmx pretyping/typing.cmx \
     proofs/logic.cmx library/libnames.cmx tactics/hipattern.cmx \
     library/global.cmx interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \
     interp/coqlib.cmx contrib/interface/pbp.cmi 
-contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \
-    contrib/interface/vtp.cmi contrib/interface/translate.cmi \
-    parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \
-    contrib/interface/ascent.cmi 
-contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \
-    contrib/interface/vtp.cmx contrib/interface/translate.cmx \
-    parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \
-    contrib/interface/ascent.cmi 
 contrib/interface/showproof.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     pretyping/typing.cmi kernel/typeops.cmi contrib/interface/translate.cmi \
     pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi \
@@ -3411,6 +3405,14 @@ contrib/interface/showproof.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
     interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \
     kernel/declarations.cmx interp/constrintern.cmx pretyping/clenv.cmx \
     contrib/interface/showproof.cmi 
+contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \
+    contrib/interface/vtp.cmi contrib/interface/translate.cmi \
+    parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \
+    contrib/interface/ascent.cmi 
+contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \
+    contrib/interface/vtp.cmx contrib/interface/translate.cmx \
+    parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \
+    contrib/interface/ascent.cmi 
 contrib/interface/translate.cmo: contrib/interface/xlate.cmi \
     contrib/interface/vtp.cmi toplevel/vernacinterp.cmi lib/util.cmi \
     kernel/term.cmi proofs/tacmach.cmi kernel/sign.cmi proofs/proof_type.cmi \
@@ -3679,16 +3681,12 @@ contrib/subtac/context.cmo: kernel/term.cmi kernel/names.cmi \
     contrib/subtac/context.cmi 
 contrib/subtac/context.cmx: kernel/term.cmx kernel/names.cmx \
     contrib/subtac/context.cmi 
-contrib/subtac/eterm.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
-    tactics/tacticals.cmi contrib/subtac/subtac_utils.cmi parsing/printer.cmi \
-    lib/pp.cmi lib/options.cmi kernel/names.cmi library/global.cmi \
-    pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \
-    contrib/subtac/eterm.cmi 
-contrib/subtac/eterm.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \
-    tactics/tacticals.cmx contrib/subtac/subtac_utils.cmx parsing/printer.cmx \
-    lib/pp.cmx lib/options.cmx kernel/names.cmx library/global.cmx \
-    pretyping/evd.cmx pretyping/evarutil.cmx kernel/environ.cmx \
-    contrib/subtac/eterm.cmi 
+contrib/subtac/eterm.cmo: lib/util.cmi kernel/term.cmi tactics/tacticals.cmi \
+    lib/pp.cmi lib/options.cmi kernel/names.cmi pretyping/evd.cmi \
+    pretyping/evarutil.cmi kernel/environ.cmi contrib/subtac/eterm.cmi 
+contrib/subtac/eterm.cmx: lib/util.cmx kernel/term.cmx tactics/tacticals.cmx \
+    lib/pp.cmx lib/options.cmx kernel/names.cmx pretyping/evd.cmx \
+    pretyping/evarutil.cmx kernel/environ.cmx contrib/subtac/eterm.cmi 
 contrib/subtac/g_eterm.cmo: lib/util.cmi proofs/tacmach.cmi \
     tactics/tacinterp.cmi proofs/tacexpr.cmo proofs/refiner.cmi \
     parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi contrib/subtac/eterm.cmi \
@@ -3711,46 +3709,76 @@ contrib/subtac/g_subtac.cmx: toplevel/vernacinterp.cmx \
     kernel/reduction.cmx lib/pp.cmx parsing/pcoq.cmx lib/options.cmx \
     kernel/names.cmx library/nameops.cmx library/libnames.cmx \
     interp/genarg.cmx parsing/egrammar.cmx toplevel/cerrors.cmx 
+contrib/subtac/subtac.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
+    kernel/typeops.cmi kernel/type_errors.cmi pretyping/termops.cmi \
+    kernel/term.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
+    contrib/subtac/subtac_utils.cmi contrib/subtac/subtac_pretyping.cmi \
+    contrib/subtac/subtac_obligations.cmi contrib/subtac/subtac_errors.cmi \
+    contrib/subtac/subtac_command.cmi contrib/subtac/subtac_coercion.cmi \
+    kernel/sign.cmi pretyping/reductionops.cmi pretyping/recordops.cmi \
+    pretyping/rawterm.cmi parsing/printer.cmi pretyping/pretype_errors.cmi \
+    parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi pretyping/pattern.cmi \
+    lib/options.cmi library/nametab.cmi kernel/names.cmi library/library.cmi \
+    library/libnames.cmi library/lib.cmi toplevel/himsg.cmi \
+    library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
+    pretyping/evarconv.cmi contrib/subtac/eterm.cmi kernel/environ.cmi \
+    lib/dyn.cmi library/decl_kinds.cmo interp/coqlib.cmi \
+    contrib/subtac/context.cmi toplevel/command.cmi pretyping/classops.cmi \
+    toplevel/cerrors.cmi contrib/subtac/subtac.cmi 
+contrib/subtac/subtac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
+    kernel/typeops.cmx kernel/type_errors.cmx pretyping/termops.cmx \
+    kernel/term.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
+    contrib/subtac/subtac_utils.cmx contrib/subtac/subtac_pretyping.cmx \
+    contrib/subtac/subtac_obligations.cmx contrib/subtac/subtac_errors.cmx \
+    contrib/subtac/subtac_command.cmx contrib/subtac/subtac_coercion.cmx \
+    kernel/sign.cmx pretyping/reductionops.cmx pretyping/recordops.cmx \
+    pretyping/rawterm.cmx parsing/printer.cmx pretyping/pretype_errors.cmx \
+    parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx pretyping/pattern.cmx \
+    lib/options.cmx library/nametab.cmx kernel/names.cmx library/library.cmx \
+    library/libnames.cmx library/lib.cmx toplevel/himsg.cmx \
+    library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
+    pretyping/evarconv.cmx contrib/subtac/eterm.cmx kernel/environ.cmx \
+    lib/dyn.cmx library/decl_kinds.cmx interp/coqlib.cmx \
+    contrib/subtac/context.cmx toplevel/command.cmx pretyping/classops.cmx \
+    toplevel/cerrors.cmx contrib/subtac/subtac.cmi 
 contrib/subtac/subtac_cases.cmo: lib/util.cmi kernel/typeops.cmi \
     kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \
     contrib/subtac/subtac_utils.cmi kernel/sign.cmi pretyping/retyping.cmi \
-    pretyping/reductionops.cmi pretyping/rawterm.cmi parsing/printer.cmi \
-    pretyping/pretype_errors.cmi parsing/prettyp.cmi lib/pp.cmi \
-    kernel/names.cmi library/nameops.cmi pretyping/inductiveops.cmi \
-    kernel/inductive.cmi library/global.cmi pretyping/evd.cmi \
-    pretyping/evarutil.cmi pretyping/evarconv.cmi kernel/environ.cmi \
-    kernel/declarations.cmi pretyping/coercion.cmi kernel/closure.cmi \
-    contrib/subtac/subtac_cases.cmi 
+    pretyping/reductionops.cmi pretyping/rawterm.cmi \
+    pretyping/pretype_errors.cmi lib/pp.cmi kernel/names.cmi \
+    library/nameops.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \
+    library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
+    pretyping/evarconv.cmi kernel/environ.cmi kernel/declarations.cmi \
+    pretyping/coercion.cmi kernel/closure.cmi contrib/subtac/subtac_cases.cmi 
 contrib/subtac/subtac_cases.cmx: lib/util.cmx kernel/typeops.cmx \
     kernel/type_errors.cmx pretyping/termops.cmx kernel/term.cmx \
     contrib/subtac/subtac_utils.cmx kernel/sign.cmx pretyping/retyping.cmx \
-    pretyping/reductionops.cmx pretyping/rawterm.cmx parsing/printer.cmx \
-    pretyping/pretype_errors.cmx parsing/prettyp.cmx lib/pp.cmx \
-    kernel/names.cmx library/nameops.cmx pretyping/inductiveops.cmx \
-    kernel/inductive.cmx library/global.cmx pretyping/evd.cmx \
-    pretyping/evarutil.cmx pretyping/evarconv.cmx kernel/environ.cmx \
-    kernel/declarations.cmx pretyping/coercion.cmx kernel/closure.cmx \
-    contrib/subtac/subtac_cases.cmi 
-contrib/subtac/subtac_coercion.cmo: lib/util.cmi kernel/typeops.cmi \
-    pretyping/termops.cmi kernel/term.cmi contrib/subtac/subtac_utils.cmi \
-    contrib/subtac/subtac_errors.cmi pretyping/retyping.cmi \
-    pretyping/reductionops.cmi kernel/reduction.cmi pretyping/recordops.cmi \
-    pretyping/rawterm.cmi parsing/printer.cmi pretyping/pretype_errors.cmi \
-    lib/pp.cmi kernel/names.cmi library/nameops.cmi library/global.cmi \
-    pretyping/evd.cmi pretyping/evarutil.cmi pretyping/evarconv.cmi \
-    contrib/subtac/eterm.cmi kernel/environ.cmi interp/coqlib.cmi \
-    contrib/subtac/context.cmi pretyping/classops.cmi \
-    contrib/subtac/subtac_coercion.cmi 
-contrib/subtac/subtac_coercion.cmx: lib/util.cmx kernel/typeops.cmx \
-    pretyping/termops.cmx kernel/term.cmx contrib/subtac/subtac_utils.cmx \
-    contrib/subtac/subtac_errors.cmx pretyping/retyping.cmx \
-    pretyping/reductionops.cmx kernel/reduction.cmx pretyping/recordops.cmx \
-    pretyping/rawterm.cmx parsing/printer.cmx pretyping/pretype_errors.cmx \
-    lib/pp.cmx kernel/names.cmx library/nameops.cmx library/global.cmx \
-    pretyping/evd.cmx pretyping/evarutil.cmx pretyping/evarconv.cmx \
-    contrib/subtac/eterm.cmx kernel/environ.cmx interp/coqlib.cmx \
-    contrib/subtac/context.cmx pretyping/classops.cmx \
-    contrib/subtac/subtac_coercion.cmi 
+    pretyping/reductionops.cmx pretyping/rawterm.cmx \
+    pretyping/pretype_errors.cmx lib/pp.cmx kernel/names.cmx \
+    library/nameops.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \
+    library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
+    pretyping/evarconv.cmx kernel/environ.cmx kernel/declarations.cmx \
+    pretyping/coercion.cmx kernel/closure.cmx contrib/subtac/subtac_cases.cmi 
+contrib/subtac/subtac_coercion.cmo: lib/util.cmi pretyping/typing.cmi \
+    kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \
+    contrib/subtac/subtac_utils.cmi contrib/subtac/subtac_errors.cmi \
+    pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \
+    pretyping/recordops.cmi pretyping/rawterm.cmi parsing/printer.cmi \
+    pretyping/pretype_errors.cmi lib/pp.cmi kernel/names.cmi \
+    library/nameops.cmi library/global.cmi pretyping/evd.cmi \
+    pretyping/evarutil.cmi pretyping/evarconv.cmi contrib/subtac/eterm.cmi \
+    kernel/environ.cmi interp/coqlib.cmi contrib/subtac/context.cmi \
+    pretyping/classops.cmi contrib/subtac/subtac_coercion.cmi 
+contrib/subtac/subtac_coercion.cmx: lib/util.cmx pretyping/typing.cmx \
+    kernel/typeops.cmx pretyping/termops.cmx kernel/term.cmx \
+    contrib/subtac/subtac_utils.cmx contrib/subtac/subtac_errors.cmx \
+    pretyping/retyping.cmx pretyping/reductionops.cmx kernel/reduction.cmx \
+    pretyping/recordops.cmx pretyping/rawterm.cmx parsing/printer.cmx \
+    pretyping/pretype_errors.cmx lib/pp.cmx kernel/names.cmx \
+    library/nameops.cmx library/global.cmx pretyping/evd.cmx \
+    pretyping/evarutil.cmx pretyping/evarconv.cmx contrib/subtac/eterm.cmx \
+    kernel/environ.cmx interp/coqlib.cmx contrib/subtac/context.cmx \
+    pretyping/classops.cmx contrib/subtac/subtac_coercion.cmi 
 contrib/subtac/subtac_command.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     pretyping/typing.cmi interp/topconstr.cmi pretyping/termops.cmi \
     kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
@@ -3760,7 +3788,7 @@ contrib/subtac/subtac_command.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     contrib/subtac/subtac_obligations.cmi library/states.cmi kernel/sign.cmi \
     kernel/safe_typing.cmi interp/reserve.cmi proofs/refiner.cmi \
     pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \
-    pretyping/pretyping.cmi parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi \
+    pretyping/pretyping.cmi lib/pp.cmi proofs/pfedit.cmi \
     pretyping/pattern.cmi interp/notation.cmi library/nametab.cmi \
     kernel/names.cmi library/nameops.cmi kernel/mod_subst.cmi \
     toplevel/metasyntax.cmi pretyping/matching.cmi library/libobject.cmi \
@@ -3779,7 +3807,7 @@ contrib/subtac/subtac_command.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     contrib/subtac/subtac_obligations.cmx library/states.cmx kernel/sign.cmx \
     kernel/safe_typing.cmx interp/reserve.cmx proofs/refiner.cmx \
     pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \
-    pretyping/pretyping.cmx parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx \
+    pretyping/pretyping.cmx lib/pp.cmx proofs/pfedit.cmx \
     pretyping/pattern.cmx interp/notation.cmx library/nametab.cmx \
     kernel/names.cmx library/nameops.cmx kernel/mod_subst.cmx \
     toplevel/metasyntax.cmx pretyping/matching.cmx library/libobject.cmx \
@@ -3817,38 +3845,6 @@ contrib/subtac/subtac_interp_fixpoint.cmx: lib/util.cmx kernel/typeops.cmx \
     contrib/subtac/eterm.cmx kernel/environ.cmx lib/dyn.cmx interp/coqlib.cmx \
     contrib/subtac/context.cmx pretyping/classops.cmx \
     contrib/subtac/subtac_interp_fixpoint.cmi 
-contrib/subtac/subtac.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
-    kernel/typeops.cmi kernel/type_errors.cmi pretyping/termops.cmi \
-    kernel/term.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
-    contrib/subtac/subtac_utils.cmi contrib/subtac/subtac_pretyping.cmi \
-    contrib/subtac/subtac_obligations.cmi contrib/subtac/subtac_errors.cmi \
-    contrib/subtac/subtac_command.cmi contrib/subtac/subtac_coercion.cmi \
-    kernel/sign.cmi pretyping/reductionops.cmi pretyping/recordops.cmi \
-    pretyping/rawterm.cmi parsing/printer.cmi pretyping/pretype_errors.cmi \
-    parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi pretyping/pattern.cmi \
-    lib/options.cmi library/nametab.cmi kernel/names.cmi library/library.cmi \
-    library/libnames.cmi library/lib.cmi toplevel/himsg.cmi \
-    library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
-    pretyping/evarconv.cmi contrib/subtac/eterm.cmi kernel/environ.cmi \
-    lib/dyn.cmi library/decl_kinds.cmo interp/coqlib.cmi \
-    contrib/subtac/context.cmi toplevel/command.cmi pretyping/classops.cmi \
-    toplevel/cerrors.cmi contrib/subtac/subtac.cmi 
-contrib/subtac/subtac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
-    kernel/typeops.cmx kernel/type_errors.cmx pretyping/termops.cmx \
-    kernel/term.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
-    contrib/subtac/subtac_utils.cmx contrib/subtac/subtac_pretyping.cmx \
-    contrib/subtac/subtac_obligations.cmx contrib/subtac/subtac_errors.cmx \
-    contrib/subtac/subtac_command.cmx contrib/subtac/subtac_coercion.cmx \
-    kernel/sign.cmx pretyping/reductionops.cmx pretyping/recordops.cmx \
-    pretyping/rawterm.cmx parsing/printer.cmx pretyping/pretype_errors.cmx \
-    parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx pretyping/pattern.cmx \
-    lib/options.cmx library/nametab.cmx kernel/names.cmx library/library.cmx \
-    library/libnames.cmx library/lib.cmx toplevel/himsg.cmx \
-    library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
-    pretyping/evarconv.cmx contrib/subtac/eterm.cmx kernel/environ.cmx \
-    lib/dyn.cmx library/decl_kinds.cmx interp/coqlib.cmx \
-    contrib/subtac/context.cmx toplevel/command.cmx pretyping/classops.cmx \
-    toplevel/cerrors.cmx contrib/subtac/subtac.cmi 
 contrib/subtac/subtac_obligations.cmo: lib/util.cmi pretyping/termops.cmi \
     kernel/term.cmi library/summary.cmi contrib/subtac/subtac_utils.cmi \
     proofs/refiner.cmi pretyping/reductionops.cmi proofs/proof_type.cmi \
@@ -3867,28 +3863,6 @@ contrib/subtac/subtac_obligations.cmx: lib/util.cmx pretyping/termops.cmx \
     kernel/entries.cmx library/declare.cmx library/decl_kinds.cmx \
     toplevel/command.cmx tactics/auto.cmx \
     contrib/subtac/subtac_obligations.cmi 
-contrib/subtac/subtac_pretyping_F.cmo: lib/util.cmi kernel/typeops.cmi \
-    kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \
-    contrib/subtac/subtac_utils.cmi contrib/subtac/subtac_cases.cmi \
-    kernel/sign.cmi pretyping/retyping.cmi pretyping/reductionops.cmi \
-    pretyping/recordops.cmi pretyping/rawterm.cmi pretyping/pretyping.cmi \
-    pretyping/pretype_errors.cmi lib/pp.cmi pretyping/pattern.cmi \
-    kernel/names.cmi library/nameops.cmi library/libnames.cmi \
-    pretyping/inductiveops.cmi kernel/inductive.cmi pretyping/evd.cmi \
-    pretyping/evarutil.cmi pretyping/evarconv.cmi kernel/environ.cmi \
-    lib/dyn.cmi kernel/declarations.cmi pretyping/coercion.cmi \
-    pretyping/classops.cmi 
-contrib/subtac/subtac_pretyping_F.cmx: lib/util.cmx kernel/typeops.cmx \
-    kernel/type_errors.cmx pretyping/termops.cmx kernel/term.cmx \
-    contrib/subtac/subtac_utils.cmx contrib/subtac/subtac_cases.cmx \
-    kernel/sign.cmx pretyping/retyping.cmx pretyping/reductionops.cmx \
-    pretyping/recordops.cmx pretyping/rawterm.cmx pretyping/pretyping.cmx \
-    pretyping/pretype_errors.cmx lib/pp.cmx pretyping/pattern.cmx \
-    kernel/names.cmx library/nameops.cmx library/libnames.cmx \
-    pretyping/inductiveops.cmx kernel/inductive.cmx pretyping/evd.cmx \
-    pretyping/evarutil.cmx pretyping/evarconv.cmx kernel/environ.cmx \
-    lib/dyn.cmx kernel/declarations.cmx pretyping/coercion.cmx \
-    pretyping/classops.cmx 
 contrib/subtac/subtac_pretyping.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     kernel/typeops.cmi kernel/type_errors.cmi interp/topconstr.cmi \
     pretyping/termops.cmi kernel/term.cmi contrib/subtac/subtac_utils.cmi \
@@ -3917,6 +3891,26 @@ contrib/subtac/subtac_pretyping.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     kernel/environ.cmx lib/dyn.cmx interp/coqlib.cmx \
     contrib/subtac/context.cmx interp/constrintern.cmx pretyping/classops.cmx \
     contrib/subtac/subtac_pretyping.cmi 
+contrib/subtac/subtac_pretyping_F.cmo: lib/util.cmi kernel/typeops.cmi \
+    kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \
+    contrib/subtac/subtac_cases.cmi kernel/sign.cmi pretyping/retyping.cmi \
+    pretyping/reductionops.cmi pretyping/recordops.cmi pretyping/rawterm.cmi \
+    pretyping/pretyping.cmi pretyping/pretype_errors.cmi lib/pp.cmi \
+    pretyping/pattern.cmi kernel/names.cmi library/nameops.cmi \
+    library/libnames.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \
+    pretyping/evd.cmi pretyping/evarutil.cmi pretyping/evarconv.cmi \
+    kernel/environ.cmi lib/dyn.cmi kernel/declarations.cmi \
+    pretyping/coercion.cmi pretyping/classops.cmi 
+contrib/subtac/subtac_pretyping_F.cmx: lib/util.cmx kernel/typeops.cmx \
+    kernel/type_errors.cmx pretyping/termops.cmx kernel/term.cmx \
+    contrib/subtac/subtac_cases.cmx kernel/sign.cmx pretyping/retyping.cmx \
+    pretyping/reductionops.cmx pretyping/recordops.cmx pretyping/rawterm.cmx \
+    pretyping/pretyping.cmx pretyping/pretype_errors.cmx lib/pp.cmx \
+    pretyping/pattern.cmx kernel/names.cmx library/nameops.cmx \
+    library/libnames.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \
+    pretyping/evd.cmx pretyping/evarutil.cmx pretyping/evarconv.cmx \
+    kernel/environ.cmx lib/dyn.cmx kernel/declarations.cmx \
+    pretyping/coercion.cmx pretyping/classops.cmx 
 contrib/subtac/subtac_utils.cmo: lib/util.cmi interp/topconstr.cmi \
     pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \
     tactics/tacticals.cmi proofs/tacexpr.cmo kernel/reduction.cmi \
@@ -3937,12 +3931,18 @@ contrib/subtac/subtac_utils.cmx: lib/util.cmx interp/topconstr.cmx \
     pretyping/evarutil.cmx kernel/entries.cmx library/decl_kinds.cmx \
     interp/coqlib.cmx interp/constrextern.cmx toplevel/command.cmx \
     contrib/subtac/subtac_utils.cmi 
+contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi 
+contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx 
 contrib/xml/acic2Xml.cmo: contrib/xml/xml.cmi lib/util.cmi kernel/term.cmi \
     kernel/names.cmi contrib/xml/cic2acic.cmo contrib/xml/acic.cmo 
 contrib/xml/acic2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx kernel/term.cmx \
     kernel/names.cmx contrib/xml/cic2acic.cmx contrib/xml/acic.cmx 
-contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi 
-contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx 
+contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \
+    tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \
+    contrib/xml/acic.cmo 
+contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \
+    tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \
+    contrib/xml/acic.cmx 
 contrib/xml/cic2acic.cmo: lib/util.cmi contrib/xml/unshare.cmi \
     kernel/univ.cmi kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \
     pretyping/reductionops.cmi parsing/printer.cmi lib/pp.cmi \
@@ -3961,12 +3961,6 @@ contrib/xml/cic2acic.cmx: lib/util.cmx contrib/xml/unshare.cmx \
     kernel/environ.cmx contrib/xml/doubleTypeInference.cmx \
     library/dischargedhypsmap.cmx library/declare.cmx kernel/declarations.cmx \
     contrib/xml/acic.cmx 
-contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \
-    tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \
-    contrib/xml/acic.cmo 
-contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \
-    tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \
-    contrib/xml/acic.cmx 
 contrib/xml/doubleTypeInference.cmo: lib/util.cmi contrib/xml/unshare.cmi \
     kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \
     pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \
@@ -4007,6 +4001,8 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx \
     contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx contrib/xml/acic.cmx 
 contrib/xml/unshare.cmo: contrib/xml/unshare.cmi 
 contrib/xml/unshare.cmx: contrib/xml/unshare.cmi 
+contrib/xml/xml.cmo: contrib/xml/xml.cmi 
+contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 contrib/xml/xmlcommand.cmo: contrib/xml/xml.cmi toplevel/vernac.cmi \
     lib/util.cmi contrib/xml/unshare.cmi kernel/typeops.cmi kernel/term.cmi \
     proofs/tacmach.cmi pretyping/recordops.cmi proofs/proof_trees.cmi \
@@ -4037,10 +4033,12 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \
     toplevel/vernacinterp.cmx lib/util.cmx lib/pp.cmx parsing/pcoq.cmx \
     parsing/lexer.cmx interp/genarg.cmx parsing/extend.cmx \
     parsing/egrammar.cmx toplevel/cerrors.cmx 
-contrib/xml/xml.cmo: contrib/xml/xml.cmi 
-contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 ide/utils/config_file.cmo: ide/utils/config_file.cmi 
 ide/utils/config_file.cmx: ide/utils/config_file.cmi 
+ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \
+    ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi 
+ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \
+    ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi 
 ide/utils/configwin_html_config.cmo: ide/utils/configwin_types.cmo \
     ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmo \
     ide/utils/config_file.cmi 
@@ -4051,10 +4049,6 @@ ide/utils/configwin_ihm.cmo: ide/utils/okey.cmi ide/utils/configwin_types.cmo \
     ide/utils/configwin_messages.cmo ide/utils/config_file.cmi 
 ide/utils/configwin_ihm.cmx: ide/utils/okey.cmx ide/utils/configwin_types.cmx \
     ide/utils/configwin_messages.cmx ide/utils/config_file.cmx 
-ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \
-    ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi 
-ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \
-    ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi 
 ide/utils/configwin_types.cmo: ide/utils/configwin_keys.cmo \
     ide/utils/config_file.cmi 
 ide/utils/configwin_types.cmx: ide/utils/configwin_keys.cmx \
diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
index 8d7fd1f18..d93350fa5 100644
--- a/parsing/g_decl_mode.ml4
+++ b/parsing/g_decl_mode.ml4
@@ -50,18 +50,26 @@ GLOBAL: proof_instr;
       | c=constr -> {st_label=Anonymous;st_it=This c}
       ]
     ];
-  justification : 
-    [[ -> Automated [] 
-     | IDENT "by"; l=LIST1 constr SEP "," -> Automated l
-     | IDENT "by"; IDENT "tactic"; tac=tactic -> By_tactic tac ]]
+  justification_items : 
+    [[ -> Some [] 
+     | IDENT "by"; l=LIST1 constr SEP "," -> Some l
+     | IDENT "by"; "*"                    -> None ]]
+  ;
+  justification_method : 
+    [[ -> None 
+     | "using";  tac = tactic -> Some tac ]]
   ;
   simple_cut_or_thesis :
     [[ ls = statement_or_thesis;
-       j=justification -> {cut_stat=ls;cut_by=j} ]]
+       j = justification_items;
+       taco = justification_method 	
+	 -> {cut_stat=ls;cut_by=j;cut_using=taco} ]]
   ;
   simple_cut :
     [[ ls = statement;
-       j=justification -> {cut_stat=ls;cut_by=j} ]]
+       j = justification_items;
+       taco = justification_method 	
+	 -> {cut_stat=ls;cut_by=j;cut_using=taco} ]]
   ;
   elim_type:
     [[ IDENT "induction" -> ET_Induction
diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml
index 7e57885cb..6e1944b2c 100644
--- a/parsing/ppdecl_proof.ml
+++ b/parsing/ppdecl_proof.ml
@@ -22,13 +22,17 @@ let pr_label = function
     Anonymous -> mt ()
   | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () 
 
-let pr_justification env = function
-    Automated [] -> mt ()
-  | Automated (_::_ as l) -> 
+let pr_justification_items env = function
+    Some [] -> mt ()
+  | Some (_::_ as l) -> 
       spc () ++ str "by" ++ spc () ++  
 	prlist_with_sep (fun () -> str ",") (pr_constr env) l
-  | By_tactic tac -> 
-      spc () ++ str "by" ++ spc () ++ str "tactic" ++  pr_tac env tac
+  | None -> spc () ++ str "by *"
+
+let pr_justification_method env = function
+    None -> mt ()
+  | Some tac -> 
+      spc () ++ str "using" ++  pr_tac env tac
 
 let pr_statement pr_it env st = 
   pr_label st.st_label ++ pr_it env st.st_it
@@ -42,7 +46,8 @@ let pr_or_thesis pr_this env = function
 
 let pr_cut pr_it env c = 
   hov 1 (pr_statement pr_it env c.cut_stat) ++ 
-    pr_justification env c.cut_by
+    pr_justification_items env c.cut_by ++
+    pr_justification_method env c.cut_using
 
 let type_or_thesis = function
     Thesis _ -> Term.mkProp
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
index 24af3842c..67a1ea5a6 100644
--- a/proofs/decl_expr.mli
+++ b/proofs/decl_expr.mli
@@ -12,10 +12,6 @@ open Names
 open Util
 open Tacexpr
 
-type ('constr,'tac) justification =
-  By_tactic of 'tac
-| Automated of 'constr list
-
 type 'it statement = 
     {st_label:name;
      st_it:'it}
@@ -43,7 +39,8 @@ type block_type =
 
 type ('it,'constr,'tac) cut =
     {cut_stat: 'it statement;
-     cut_by: ('constr,'tac) justification}
+     cut_by: 'constr list option;
+     cut_using: 'tac option}
 
 type ('var,'constr) hyp = 
     Hvar of 'var 
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 8ace0a085..beda24629 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -22,9 +22,11 @@ open Pp
 
 let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) 
 
-let intern_justification globs = function
-    Automated l -> Automated (List.map (intern_constr globs) l)
-  | By_tactic tac -> By_tactic (intern_tactic globs tac) 
+let intern_justification_items globs = 
+  option_map (List.map (intern_constr globs))
+
+let intern_justification_method globs = 
+  option_map (intern_tactic globs)
 
 let intern_statement intern_it globs st =
   {st_label=st.st_label;
@@ -54,7 +56,8 @@ let intern_hyps iconstr globs hyps =
 
 let intern_cut intern_it globs cut=
  {cut_stat=intern_statement intern_it globs cut.cut_stat;
-  cut_by=intern_justification globs cut.cut_by}
+  cut_by=intern_justification_items globs cut.cut_by;
+  cut_using=intern_justification_method globs cut.cut_using}
 
 let intern_casee globs = function 
     Real c -> Real (intern_constr globs c)
@@ -118,10 +121,8 @@ let rec intern_proof_instr globs instr=
   {emph = instr.emph;
    instr = intern_bare_proof_instr globs instr.instr}
 
-let interp_justification env sigma  = function
-    Automated l -> 
-      Automated (List.map (fun c ->understand env sigma (fst c)) l)
-  | By_tactic tac -> By_tactic tac 
+let interp_justification_items env sigma  =
+    option_map (List.map (fun c ->understand env sigma (fst c)))
 
 let interp_constr check_sort env sigma c = 
   if check_sort then 
@@ -368,8 +369,9 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
 	     pat_expr=pat},thyps
 
 let interp_cut interp_it env sigma cut=
- {cut_stat=interp_statement interp_it env sigma cut.cut_stat;
-  cut_by=interp_justification env sigma cut.cut_by}
+  {cut with 
+    cut_stat=interp_statement interp_it env sigma cut.cut_stat;
+    cut_by=interp_justification_items env sigma cut.cut_by}
 
 let interp_casee env sigma = function 
     Real c -> Real (understand env sigma (fst c))
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 2e3e0d3c8..244cb288e 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -259,13 +259,12 @@ let add_justification_hyps keep items gls =
 	    letin_tac false (Names.Name id) c Tacexpr.nowhere gls in 
     tclMAP add_aux items gls   
 
-let apply_to_prepared_goal items kont gls =
+let prepare_goal items gls =
   let tokeep = ref Idset.empty in
   let auxres = add_justification_hyps tokeep items gls in
    tclTHENLIST
      [ (fun _ -> auxres);
-       filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep);
-       kont ] gls
+       filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep)] gls
 
 let my_automation_tac = ref 
   (fun gls -> anomaly "No automation registered")
@@ -276,7 +275,7 @@ let automation_tac gls = !my_automation_tac gls
 
 let justification tac gls= 
     tclORELSE 
-      (tclSOLVE [tac]) 
+      (tclSOLVE [tclTHEN tac assumption]) 
       (fun gls -> 
 	 if get_strictness () then 
 	   error "insufficient justification" 
@@ -286,8 +285,8 @@ let justification tac gls=
 	     daimon_tac gls
 	   end) gls
 
-let default_justification items gls=
-  justification (apply_to_prepared_goal items automation_tac) gls
+let default_justification elems gls=
+  justification (tclTHEN (prepare_goal elems) automation_tac) gls
 
 (* code for have/then/thus/hence *)
 
@@ -452,19 +451,26 @@ let mk_stat_or_thesis info = function
 	    "\"thesis\" is split, please specify which part you refer to."
 			
 let instr_cut mkstat _thus _then cut gls0 = 
-  let info = get_its_info gls0 in  
-  let just_tac gls = 
+  let info = get_its_info gls0 in
+  let items_tac gls =
     match cut.cut_by with
-        Automated l ->	
-	  let elems = 
+	None -> tclIDTAC gls
+      | Some items -> 
+	  let items_ = 
 	    if _then then
 	      match info.pm_last with
-		  Anonymous -> l
-		| Name id -> (mkVar id) ::l
-	    else l in
-	    default_justification elems gls
-      | By_tactic t -> 
-	  justification (Tacinterp.eval_tactic t) gls in
+		  Anonymous -> error "no previous statement to use"
+		| Name id -> (mkVar id)::items
+	    else items
+	  in prepare_goal items_ gls in
+  let method_tac gls = 
+    match cut.cut_using with
+        None ->	
+	  automation_tac gls
+      | Some tac -> 
+	  (Tacinterp.eval_tactic tac) gls in
+  let just_tac gls =
+    justification (tclTHEN items_tac method_tac) gls in
   let c_id = match cut.cut_stat.st_label with 
       Anonymous -> 
 	pf_get_new_id (id_of_string "_fact") gls0 
@@ -501,13 +507,18 @@ let instr_rew _thus rew_side cut gls0 =
 	Anonymous -> error "no previous equality"
       | Name id -> id in
   let typ,lhs,rhs = decompose_eq last_id gls0 in  
-  let just_tac gls = 
+  let items_tac gls =
     match cut.cut_by with
-        Automated l ->	
-	  let elems = (mkVar last_id) :: l in
-	    default_justification elems gls
-      | By_tactic t -> 
-	  justification (Tacinterp.eval_tactic t) gls in
+	None -> tclIDTAC gls
+      | Some items -> prepare_goal items gls in
+  let method_tac gls = 
+    match cut.cut_using with
+        None ->	
+	  automation_tac gls
+      | Some tac -> 
+	  (Tacinterp.eval_tactic tac) gls in
+  let just_tac gls =
+    justification (tclTHEN items_tac method_tac) gls in
   let c_id = match cut.cut_stat.st_label with 
       Anonymous -> 
 	pf_get_new_id (id_of_string "_eq") gls0 
@@ -1201,6 +1212,30 @@ let hrec_for obj_id fix_id per_info gls=
 	    else None
       | _ -> None
 
+
+(* custom elim performs the case analysis of hypothesis id from the local 
+context, 
+
+- generalizing hypotheses below id
+- computing the elimination predicate (abstract inductive predicate) 
+- build case analysis term 
+- generalize rec_calls (use wf_paths)
+- vector of introduced identifiers per branch 
+
+match id in t return p with
+ C1 ... => ?1 
+|C2 ... => ?2
+...
+end*)
+
+
+    
+
+
+
+
+
+
 let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = 
   match tree with
       Pop t ->  
@@ -1431,8 +1466,20 @@ let rec postprocess pts instr =
     | Pcut _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
     | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts
     | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> nth_unproven 1 pts
-    | Pescape ->
-	escape_command pts
+    | Pescape -> escape_command pts
+    | Pend (B_elim ET_Induction) ->
+  	begin
+	  let pf = proof_of_pftreestate pts in
+	  let (pfterm,_) = extract_open_pftreestate pts in
+	  let env =  Evd.evar_env (goal_of_proof pf) in
+	    try 
+	      Inductiveops.control_only_guard env pfterm;
+	      goto_current_focus_or_top (mark_as_done pts)
+ 	    with 
+		Type_errors.TypeError(env,
+				      Type_errors.IllFormedRecBody(_,_,_)) ->
+		  anomaly "\"end induction\" generated an ill-formed fixpoint"
+	end
     | Pend _ -> 
 	goto_current_focus_or_top (mark_as_done pts)