removes all references to ctast.ml the Makefile has been updated accordingly.

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

10 files changed, 187 insertions, 538 deletions

diff --git a/.depend b/.depend
index 9c5ccbe405..e421db2a5b 100644
--- a/.depend
+++ b/.depend
@@ -38,10 +38,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/univ.cmi 
 kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
-kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi 
 kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi 
+kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi 
 kernel/names.cmi: lib/pp.cmi lib/predicate.cmi 
 kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
@@ -61,6 +61,9 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/bignat.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 
 library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \
     kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \
     kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \
@@ -90,9 +93,6 @@ library/nameops.cmi: kernel/names.cmi lib/pp.cmi
 library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi lib/util.cmi 
 library/summary.cmi: library/libnames.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 interp/genarg.cmi \
     library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \
     lib/util.cmi 
@@ -304,20 +304,20 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
+toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
     library/libnames.cmi kernel/names.cmi kernel/term.cmi \
     interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: proofs/tacexpr.cmo 
-toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo 
 contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi 
 contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi 
 contrib/correctness/past.cmi: kernel/names.cmi contrib/correctness/ptype.cmi \
     kernel/term.cmi interp/topconstr.cmi lib/util.cmi 
+contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
+    pretyping/rawterm.cmi 
 contrib/correctness/pcicenv.cmi: kernel/names.cmi \
     contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
     kernel/sign.cmi kernel/term.cmi 
-contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
-    pretyping/rawterm.cmi 
 contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \
     contrib/correctness/ptype.cmi 
 contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi 
@@ -398,9 +398,8 @@ contrib/interface/translate.cmi: contrib/interface/ascent.cmi \
     kernel/environ.cmi pretyping/evd.cmi proofs/proof_type.cmi \
     kernel/term.cmi 
 contrib/interface/vtp.cmi: contrib/interface/ascent.cmi 
-contrib/interface/xlate.cmi: contrib/interface/ascent.cmi \
-    contrib/interface/ctast.cmo kernel/names.cmi proofs/tacexpr.cmo \
-    interp/topconstr.cmi toplevel/vernacexpr.cmo 
+contrib/interface/xlate.cmi: contrib/interface/ascent.cmi kernel/names.cmi \
+    proofs/tacexpr.cmo interp/topconstr.cmi 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 
@@ -552,12 +551,6 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
 kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
     kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi 
-kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
-    kernel/univ.cmi lib/util.cmi kernel/modops.cmi 
-kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
-    kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
-    kernel/univ.cmx lib/util.cmx kernel/modops.cmi 
 kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
     kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
@@ -566,6 +559,12 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
     kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
     kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
     kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi 
+kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+    kernel/univ.cmi lib/util.cmi kernel/modops.cmi 
+kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
+    kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+    kernel/univ.cmx lib/util.cmx kernel/modops.cmi 
 kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \
     kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \
@@ -648,24 +647,34 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
 lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi 
 lib/explore.cmo: lib/explore.cmi 
 lib/explore.cmx: lib/explore.cmi 
-lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
-lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
 lib/gmap.cmo: lib/gmap.cmi 
 lib/gmap.cmx: lib/gmap.cmi 
+lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
+lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.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/pp.cmi lib/util.cmi lib/rtree.cmi 
+lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
+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 
 library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \
     library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \
     library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
@@ -770,16 +779,6 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
     lib/system.cmx library/states.cmi 
 library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi 
-lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi 
-lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
-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/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \
     parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
     toplevel/vernacexpr.cmo 
@@ -1770,10 +1769,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.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.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
-tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
 tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
 tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
 tools/gallina.cmo: tools/gallina_lexer.cmo 
 tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
@@ -1976,6 +1975,16 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \
     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/vernac.cmo: parsing/coqast.cmi library/lib.cmi library/library.cmi \
+    kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \
+    toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: parsing/coqast.cmx library/lib.cmx library/library.cmx \
+    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
+    lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \
+    toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \
     pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \
     interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \
@@ -2036,16 +2045,6 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.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/coqast.cmi library/lib.cmi library/library.cmi \
-    kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
-    lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \
-    toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
-    toplevel/vernacinterp.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/coqast.cmx library/lib.cmx library/library.cmx \
-    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
-    lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \
-    toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
-    toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi contrib/cc/ccalgo.cmi 
 contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx contrib/cc/ccalgo.cmi 
 contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi \
@@ -2066,18 +2065,6 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
     lib/pp.cmx parsing/pptactic.cmx proofs/proof_type.cmx proofs/refiner.cmx \
     tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
-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 \
-    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
-contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
-    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
-    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
 contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \
     pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \
     kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \
@@ -2094,6 +2081,18 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \
     kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
     interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx contrib/correctness/pcic.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 \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
+    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/univ.cmx contrib/correctness/pcicenv.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 \
@@ -2499,7 +2498,6 @@ contrib/interface/blast.cmx: tactics/auto.cmx proofs/clenv.cmx \
 contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     contrib/interface/blast.cmi toplevel/cerrors.cmi pretyping/classops.cmi \
     toplevel/command.cmi interp/constrintern.cmi parsing/coqast.cmi \
-    contrib/interface/ctast.cmo contrib/interface/dad.cmi \
     contrib/interface/debug_tac.cmi kernel/declarations.cmi \
     library/declare.cmi parsing/egrammar.cmi kernel/environ.cmi \
     pretyping/evd.cmi parsing/extend.cmi interp/genarg.cmi library/global.cmi \
@@ -2521,7 +2519,6 @@ contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
 contrib/interface/centaur.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \
     contrib/interface/blast.cmx toplevel/cerrors.cmx pretyping/classops.cmx \
     toplevel/command.cmx interp/constrintern.cmx parsing/coqast.cmx \
-    contrib/interface/ctast.cmx contrib/interface/dad.cmx \
     contrib/interface/debug_tac.cmx kernel/declarations.cmx \
     library/declare.cmx parsing/egrammar.cmx kernel/environ.cmx \
     pretyping/evd.cmx parsing/extend.cmx interp/genarg.cmx library/global.cmx \
@@ -2545,25 +2542,25 @@ contrib/interface/ctast.cmo: parsing/coqast.cmi lib/dyn.cmi \
 contrib/interface/ctast.cmx: parsing/coqast.cmx lib/dyn.cmx \
     library/libnames.cmx kernel/names.cmx lib/util.cmx 
 contrib/interface/dad.cmo: interp/constrextern.cmi interp/constrintern.cmi \
-    contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evd.cmi \
-    interp/genarg.cmi library/global.cmi library/libnames.cmi \
-    kernel/names.cmi library/nametab.cmi contrib/interface/paths.cmi \
-    pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
-    proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi kernel/term.cmi interp/topconstr.cmi \
-    pretyping/typing.cmi lib/util.cmi toplevel/vernacexpr.cmo \
-    toplevel/vernacinterp.cmi contrib/interface/dad.cmi 
+    kernel/environ.cmi pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
+    library/libnames.cmi kernel/names.cmi library/nametab.cmi \
+    contrib/interface/paths.cmi pretyping/pattern.cmi lib/pp.cmi \
+    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
+    kernel/reduction.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+    interp/topconstr.cmi pretyping/typing.cmi lib/util.cmi \
+    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi \
+    contrib/interface/dad.cmi 
 contrib/interface/dad.cmx: interp/constrextern.cmx interp/constrintern.cmx \
-    contrib/interface/ctast.cmx kernel/environ.cmx pretyping/evd.cmx \
-    interp/genarg.cmx library/global.cmx library/libnames.cmx \
-    kernel/names.cmx library/nametab.cmx contrib/interface/paths.cmx \
-    pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \
-    proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
-    proofs/tacexpr.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx kernel/term.cmx interp/topconstr.cmx \
-    pretyping/typing.cmx lib/util.cmx toplevel/vernacexpr.cmx \
-    toplevel/vernacinterp.cmx contrib/interface/dad.cmi 
+    kernel/environ.cmx pretyping/evd.cmx interp/genarg.cmx library/global.cmx \
+    library/libnames.cmx kernel/names.cmx library/nametab.cmx \
+    contrib/interface/paths.cmx pretyping/pattern.cmx lib/pp.cmx \
+    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
+    kernel/reduction.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+    interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \
+    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx \
+    contrib/interface/dad.cmi 
 contrib/interface/debug_tac.cmo: parsing/ast.cmi toplevel/cerrors.cmi \
     parsing/coqast.cmi interp/genarg.cmi lib/pp.cmi parsing/pptactic.cmi \
     proofs/proof_trees.cmi proofs/proof_type.cmi proofs/refiner.cmi \
@@ -2616,32 +2613,24 @@ contrib/interface/parse.cmx: contrib/interface/ascent.cmi \
     contrib/interface/xlate.cmx 
 contrib/interface/paths.cmo: contrib/interface/paths.cmi 
 contrib/interface/paths.cmx: contrib/interface/paths.cmi 
-contrib/interface/pbp.cmo: interp/coqlib.cmi contrib/interface/ctast.cmo \
-    kernel/environ.cmi pretyping/evd.cmi library/global.cmi \
-    tactics/hipattern.cmi library/libnames.cmi proofs/logic.cmi \
-    kernel/names.cmi library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
+contrib/interface/pbp.cmo: interp/coqlib.cmi kernel/environ.cmi \
+    pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \
+    library/libnames.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 interp/topconstr.cmi \
     pretyping/typing.cmi lib/util.cmi contrib/interface/pbp.cmi 
-contrib/interface/pbp.cmx: interp/coqlib.cmx contrib/interface/ctast.cmx \
-    kernel/environ.cmx pretyping/evd.cmx library/global.cmx \
-    tactics/hipattern.cmx library/libnames.cmx proofs/logic.cmx \
-    kernel/names.cmx library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \
+contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \
+    pretyping/evd.cmx library/global.cmx tactics/hipattern.cmx \
+    library/libnames.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 interp/topconstr.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 \
-    parsing/printer.cmi contrib/interface/translate.cmi \
-    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
-contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
-    parsing/printer.cmx contrib/interface/translate.cmx \
-    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/showproof.cmo: proofs/clenv.cmi interp/constrintern.cmi \
     parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \
     pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -2666,6 +2655,14 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.cmx \
     pretyping/termops.cmx contrib/interface/translate.cmx \
     pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/interface/showproof.cmi 
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+    parsing/printer.cmi contrib/interface/translate.cmi \
+    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+    parsing/printer.cmx contrib/interface/translate.cmx \
+    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     interp/constrextern.cmi contrib/interface/ctast.cmo kernel/environ.cmi \
     pretyping/evarutil.cmi pretyping/evd.cmi library/libobject.cmi \
@@ -2687,19 +2684,19 @@ 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 \
-    lib/bignat.cmi contrib/interface/ctast.cmo library/decl_kinds.cmo \
-    tactics/eauto.cmo tactics/extraargs.cmi interp/genarg.cmi \
-    library/goptions.cmi library/libnames.cmi kernel/names.cmi \
-    lib/options.cmi parsing/ppconstr.cmi pretyping/rawterm.cmi \
-    proofs/tacexpr.cmo kernel/term.cmi interp/topconstr.cmi lib/util.cmi \
-    toplevel/vernacexpr.cmo contrib/interface/xlate.cmi 
+    lib/bignat.cmi library/decl_kinds.cmo tactics/eauto.cmo \
+    tactics/extraargs.cmi interp/genarg.cmi library/goptions.cmi \
+    library/libnames.cmi kernel/names.cmi lib/options.cmi \
+    parsing/ppconstr.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \
+    kernel/term.cmi interp/topconstr.cmi lib/util.cmi toplevel/vernacexpr.cmo \
+    contrib/interface/xlate.cmi 
 contrib/interface/xlate.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \
-    lib/bignat.cmx contrib/interface/ctast.cmx library/decl_kinds.cmx \
-    tactics/eauto.cmx tactics/extraargs.cmx interp/genarg.cmx \
-    library/goptions.cmx library/libnames.cmx kernel/names.cmx \
-    lib/options.cmx parsing/ppconstr.cmx pretyping/rawterm.cmx \
-    proofs/tacexpr.cmx kernel/term.cmx interp/topconstr.cmx lib/util.cmx \
-    toplevel/vernacexpr.cmx contrib/interface/xlate.cmi 
+    lib/bignat.cmx library/decl_kinds.cmx tactics/eauto.cmx \
+    tactics/extraargs.cmx interp/genarg.cmx library/goptions.cmx \
+    library/libnames.cmx kernel/names.cmx lib/options.cmx \
+    parsing/ppconstr.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \
+    kernel/term.cmx interp/topconstr.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 
@@ -2838,12 +2835,12 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
     proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx lib/util.cmx 
+contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi 
+contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx 
 contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \
     kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi 
 contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \
     kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx 
-contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi 
-contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx 
 contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo library/declare.cmi \
     library/dischargedhypsmap.cmi contrib/xml/doubleTypeInference.cmi \
     kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
@@ -2898,6 +2895,8 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \
     contrib/xml/xml.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/acic.cmo contrib/xml/acic2Xml.cmo \
     contrib/xml/cic2acic.cmo library/decl_kinds.cmo kernel/declarations.cmi \
     library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
@@ -2924,8 +2923,6 @@ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     parsing/extend.cmx interp/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
 tactics/tauto.cmx: parsing/grammar.cma
 tactics/eqdecide.cmo: parsing/grammar.cma
diff --git a/Makefile b/Makefile
index 6302cc3054..6d8a8decfe 100644
--- a/Makefile
+++ b/Makefile
@@ -183,8 +183,7 @@ USERTACCMO=$(USERTAC:.ml4=.cmo)
 USERTACCMX=$(USERTAC:.ml4=.cmx)
 
 INTERFACE=\
-  contrib/interface/vtp.cmo \
-  contrib/interface/ctast.cmo contrib/interface/xlate.cmo \
+  contrib/interface/vtp.cmo contrib/interface/xlate.cmo \
   contrib/interface/paths.cmo contrib/interface/translate.cmo \
   contrib/interface/pbp.cmo \
   contrib/interface/dad.cmo \
@@ -415,10 +414,10 @@ hightactics: $(HIGHTACTICS)
 bin/coq-interface$(EXE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(INTERFACE)
 	$(COQMKTOP) -top $(BYTEFLAGS) -o $@ $(INTERFACE)
 
-bin/parser$(EXE): contrib/interface/ctast.cmo contrib/interface/parse.cmo contrib/interface/line_parser.cmo $(PARSERREQUIRES) contrib/interface/xlate.cmo contrib/interface/vtp.cmo
+bin/parser$(EXE): contrib/interface/parse.cmo contrib/interface/line_parser.cmo $(PARSERREQUIRES) contrib/interface/xlate.cmo contrib/interface/vtp.cmo
 	$(OCAMLC) -cclib -lunix -custom $(BYTEFLAGS) -o $@ $(CMA) \
 	$(PARSERREQUIRES) \
-	ctast.cmo line_parser.cmo vtp.cmo xlate.cmo parse.cmo
+	line_parser.cmo vtp.cmo xlate.cmo parse.cmo
 
 clean::
 	rm -f bin/parser$(EXE) bin/coq-interface$(EXE)
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index b62339fa5d..a729632938 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -228,10 +228,11 @@ and ct_FORMULA =
   | CT_bang of ct_INT_OPT * ct_FORMULA
   | CT_cases of ct_FORMULA_OPT * ct_FORMULA_NE_LIST * ct_EQN_LIST
   | CT_cofixc of ct_ID * ct_COFIX_REC_LIST
-  | CT_elimc of ct_CASE * ct_FORMULA * ct_FORMULA * ct_FORMULA_LIST
+  | CT_elimc of ct_CASE * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA_LIST
   | CT_existvarc
   | CT_fixc of ct_ID * ct_FIX_BINDER_LIST
   | CT_if of ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA * ct_FORMULA
+  | CT_inductive_let of ct_FORMULA_OPT * ct_ID_OPT_NE_LIST * ct_FORMULA * ct_FORMULA
   | CT_int_encapsulator of string
   | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
   | CT_letin of ct_DEF * ct_FORMULA
@@ -519,7 +520,7 @@ and ct_TACTIC_COM =
   | CT_split of ct_SPEC_LIST
   | CT_superauto of ct_INT_OPT * ct_ID_LIST * ct_DESTRUCTING * ct_USINGTDB
   | CT_symmetry
-  | CT_tac_double of ct_INT * ct_INT
+  | CT_tac_double of ct_ID_OR_INT * ct_ID_OR_INT
   | CT_tacsolve of ct_TACTIC_COM * ct_TACTIC_COM list
   | CT_tactic_fun of ct_ID_UNIT_LIST * ct_TACTIC_COM
   | CT_then of ct_TACTIC_COM * ct_TACTIC_COM list
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 1a660a89f5..fe25cb07d3 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -37,7 +37,7 @@ open Translate;;
 open Name_to_ast;;
 open Pbp;;
 open Blast;;
-open Dad;;
+(* open Dad;; *)
 open Debug_tac;;
 open Search;;
 open Constrintern;;
@@ -330,11 +330,13 @@ let globcv x =
 	       (ConstructRef ((sp, tyi), i)))
   | _ -> failwith "globcv : unexpected value";;
 
+(* <\cpa> 
 let pbp_tac_pcoq =
     pbp_tac (function (x:raw_tactic_expr) -> 
       output_results
         (ctf_header "pbp_results" !global_request_id)
        (Some (P_t(xlate_tactic x))));;
+</cpa> *)
 
 let blast_tac_pcoq =
     blast_tac (function (x:raw_tactic_expr) -> 
@@ -342,12 +344,13 @@ let blast_tac_pcoq =
 	(ctf_header "pbp_results" !global_request_id)
        (Some (P_t(xlate_tactic x))));;
 
-
+(* <\cpa> 
 let dad_tac_pcoq =
   dad_tac(function x -> 
     output_results
     (ctf_header "pbp_results" !global_request_id)
     (Some (P_t(xlate_tactic x))));;
+</cpa> *)
 
 let search_output_results () =
   output_results
@@ -551,6 +554,9 @@ let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s)
 let pcoq_search s l =
   ctv_SEARCH_LIST:=[];
   begin match s with
+  | SearchAbout locqid -> 
+      raw_search_about (filter_by_module_from_list l) add_search
+	(Nametab.global locqid)
   | SearchPattern c ->
       let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
       raw_pattern_search (filter_by_module_from_list l) add_search pat
@@ -573,7 +579,7 @@ let pcoq_print_check j =
   let a,b = print_check j in output_results a b
 
 let pcoq_print_eval redfun env c j =
-  let strm, vtp = ct_print_eval (Ctast.ast_to_ct c) redfun env j in
+  let strm, vtp = ct_print_eval c redfun env j in
   output_results strm vtp;;
 
 open Vernacentries
@@ -879,6 +885,7 @@ let command_creations = [
 ];;
 *)
 
+(* <\cpa> 
 TACTIC EXTEND Pbp
 | [ "Pbp" ident_opt(idopt) natural_list(nl) ] -> 
     [ if_pcoq pbp_tac_pcoq idopt nl ]
@@ -891,6 +898,7 @@ TACTIC EXTEND Dad
 | [ "Dad" natural_list(nl1) "to" natural_list(nl2) ] ->
     [ if_pcoq dad_tac_pcoq nl1 nl2 ]
 END
+ </cpa> *)
 
 TACTIC EXTEND CtDebugTac
 | [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq t ]
@@ -904,8 +912,9 @@ END
 let start_pcoq_mode debug = 
   begin
     pcoq_started := Some debug;
+(* <\cpa> 
     start_dad();
-    set_xlate_mut_stuff (fun x ->Ctast.ast_to_ct (globcv (Ctast.ct_to_ast x)));
+</cpa> *)
     declare_in_coq();
 (*
     add_tactic "PcoqPbp" pbp_tac_pcoq;
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index 00a4bb07ec..4f03fb06fd 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -11,7 +11,6 @@ open Tactics;;
 open Tacticals;;
 open Pattern;;
 open Reduction;;
-open Ctast;;
 open Constrextern;;
 open Constrintern;;
 open Vernacinterp;;
@@ -47,9 +46,7 @@ type dad_rule =
     constr_expr * int list * int list * int * int list
     * raw_atomic_tactic_expr;;
 
-(* This value will be used systematically when constructing objects of
-   type Ctast.t, the value is stupid and meaningless, but it is needed
-   to construct well-typed terms. *)
+(* This value will be used systematically when constructing objects *)
 
 let zz = (0,0);;
 
@@ -70,17 +67,7 @@ let rec get_subterm  (depth:int) (path: int list) (constr:constr) =
    first argument, an object of type env, is necessary to
    transform constr terms into abstract syntax trees.  The second argument is
    the substitution, a list of pairs linking an integer and a constr term. *)
-(*
-let map_subst (env :env) 
-   (subst:(int * Term.constr) list) =
-   let rec map_subst_aux = function
-    Coqast.Node(_, "META", [Coqast.Num(_, i)]) ->
-      let constr = List.assoc i subst in
-      ast_of_constr false env constr
-  | Coqast.Node(loc, s, l) -> Coqast.Node(loc, s, List.map map_subst_aux l)
-  | ast -> ast in
-    map_subst_aux;;
-*)
+
 let rec map_subst (env :env) (subst:(int * Term.constr) list) = function
   | CMeta (_,i) ->
       let constr = List.assoc i subst in
@@ -274,7 +261,7 @@ let start_dad () = dad_status := true;;
 
 let add_dad_rule_fn name pat p1 p2 tac =
   let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in
-  add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr tac;;
+  add_dad_rule name pat p1 p2 (List.length pr) pr tac;;
 
 (* To be parsed by camlp4
 
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 80009d7838..039127cc56 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -155,17 +155,7 @@ let make_variable_ast name typ implicits =
     ((Local,Definitional), [false,(name, constr_to_ast (body_of_type typ))]))
   ::(implicits_to_ast_list implicits);;
     
-(*
-let make_definition_ast name c typ implicits =
- (ope("DEFINITION",
-      [string "DEFINITION";
-       nvar name;
-       ope("COMMAND",
-           [ope("CAST",
-                [(constr_to_ast c);
-		 (constr_to_ast (body_of_type typ))])])]))::
-  (implicits_to_ast_list implicits);;
-*)
+
 let make_definition_ast name c typ implicits =
   VernacDefinition (Global, name, DefineBody ([], None,
     (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index bc9f706c57..d4d134f647 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -7,7 +7,6 @@ open Tacticals;;
 open Hipattern;;
 open Pattern;;
 open Reduction;;
-open Ctast;;
 open Rawterm;;
 open Environ;;
 
@@ -88,34 +87,9 @@ type pbp_rule = (identifier list *
                        identifier option -> (types, constr) kind_of_term -> int list -> pbp_sequence)) ->
                     pbp_sequence option;;
 
-(*
-let make_named_intro s =
-    Node(zz, "Intros",
-          [Node(zz,"INTROPATTERN",
-            [Node(zz,"LISTPATTERN",
-              [Node(zz, "IDENTIFIER", 
-                [Nvar(zz, s)])])])]);;
-*)
+
 let make_named_intro id = PbpIntros [id]
 
-(*
-let get_name_from_intro = function
-    Node(a, "Intros",
-          [Node(b,"INTROPATTERN",
-            [Node(c,"LISTPATTERN",
-              [Node(d, "IDENTIFIER", 
-                [Nvar(e, s)])])])]) ->
-		  Some s
-  | _ -> None;;
-*)
-(*
-let make_clears =  function
-    [] -> Node(zz, "Idtac",[])
-  | str_list ->
-      Node(zz, "TRY", [Node(zz,"Clear",
-	   [Node(zz, "CLAUSE", List.map (function s -> Nvar(zz,s)) str_list)])
-	       ]);;
-*)
 let make_clears str_list = PbpThen [PbpTryClear str_list]
 
 let add_clear_names_if_necessary tactic clear_names =
@@ -124,7 +98,6 @@ let add_clear_names_if_necessary tactic clear_names =
     | l -> chain_tactics [PbpTryClear l] tactic;;
 
 let make_final_cmd f optname clear_names constr path =
-(*    let tactic = f optname constr path in*)
     add_clear_names_if_necessary (f optname constr path) clear_names;;
 
 let (rem_cast:pbp_rule) = function
@@ -336,23 +309,7 @@ let (not_intro: pbp_rule) = function
 
 
 
-(*
-let elim_with_bindings hyp_name names =
-  Node(zz,"Elim", 
-       [Node(zz, "COMMAND", [Nvar(zz,hyp_name)]);
-	 Node(zz,"BINDINGS", 
-	      List.map 
-		(function s -> 
-		  Node(zz,"BINDING",
-		       [Nvar(zz,s);
-			 Node
-			   (zz,"COMMAND",
-			    [Node
-				(zz,"APPLIST",
-				 [Nvar(zz,"PBP_META");
-				   Nvar(zz,
-					"value_for_" ^ s)])])])) names)]);;
-*)
+
 let elim_with_bindings hyp_name names =
   PbpElim (hyp_name, names);;
 
@@ -448,114 +405,6 @@ let (mk_db_indices: int list -> int -> int list) =
    answer is true, then the built command takes advantage of the power of
    head tactics.  *)
 
-(*
-let (head_tactic_patt: pbp_rule) = function
-    avoid, clear_names, clear_flag, Some h, cstr, path, f ->
-    (match down_prods (cstr, path, 0) with
-    | (str_list, _, nprems, 
-       App(oper,[|c1|]), 2::1::path) 
-      	when
- 	  (is_matching_local (notconstr ()) oper) or
- 	  (is_matching_local (notTconstr ()) oper) ->
-	 Some(Node(zz, "TACTICLIST",
-		   [elim_with_bindings h str_list;
-		     f avoid clear_names false None (kind_of_term c1) path]))
-    | (str_list, _, nprems, 
-       App(oper, [|c1; c2|]), 2::a::path) 
-      when ((is_matching_local (andconstr()) oper) or
-	    (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) ->
-	let h1 = next_global_ident_away (id_of_string "H") avoid in
-	let str_h1 = (string_of_id h1) in
-	let h2 = next_global_ident_away (id_of_string "H") (h1::avoid) in
-	let str_h2 = (string_of_id h2) in
-	Some(Node(zz,"TACTICLIST",
-                  [elim_with_bindings h str_list;
-		    make_named_intro str_h1;
-		    make_named_intro str_h2;
-		    let cont_body = 
-		      if a = 1 then c1 else c2 in
-		    let cont_tac = 
-		      f (h2::h1::avoid) (h::clear_names) 
-                        false (Some (if 1 = a then str_h1 else str_h2))
-                        (kind_of_term cont_body) path in
-		    if nprems = 0 then
-		      cont_tac
-		    else
-		      Node(zz,"TACLIST",
-			   cont_tac::(auxiliary_goals
-					clear_names clear_flag
-					h nprems))]))
-    | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
-      when ((is_matching_local (exconstr ()) oper) or
-	    (is_matching_local (exTconstr ()) oper) or
-	    (is_matching_local (sigconstr ()) oper) or
-	    (is_matching_local (sigTconstr()) oper)) & a = 2 ->
-		   (match (kind_of_term c2),path with
-		     Lambda(Name x, _,body), (2::path) ->
-		       Some(Node(zz,"TACTICLIST",
-		    		 [elim_with_bindings h str_list;
-				   let x' = next_global_ident_away x avoid in
-				   let cont_body =
-				     Prod(Name x', c1,
-					    mkProd(Anonymous, body, 
-						   mkVar(dummy_id))) in
-				   let cont_tac 
-				       = f avoid (h::clear_names) false None
-				       cont_body (2::1::path) in
-				   if nprems = 0 then
-				     cont_tac
-				   else
-				     Node(zz,"TACLIST",
-					  cont_tac::(auxiliary_goals
-						       clear_names clear_flag
-						       h nprems))]))
-		   | _ -> None)
-    | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
-	when ((is_matching_local (orconstr ()) oper) or
-              (is_matching_local (sumboolconstr ()) oper) or
-	      (is_matching_local (sumconstr ()) oper)) &
-                (a = 1 or a = 2) ->
-	  Some(Node(zz, "TACTICLIST",
-		    [elim_with_bindings h str_list;
-		      let cont_body =
-			if a = 1 then c1 else c2 in
-                      (* h' is the name for the new intro *)
-		      let h' = next_global_ident_away (id_of_string "H") avoid in
-		      let str_h' = (string_of_id h') in
-		      let cont_tac =
-                        Node(zz,"TACTICLIST",
-			     [make_named_intro str_h';
-			       f 
-				 (* h' should not be used again *)
-				 (h'::avoid)
-				 (* the disjunct itself can be discarded *)
-				 (h::clear_names) false (Some str_h')
-                          (kind_of_term cont_body) path]) in
-		      let snd_tac = 
-			Node(zz, "TACTICLIST", 
-			     [make_named_intro str_h';
-			       make_clears (h::clear_names)]) in
-		      let tacs1 = 
-			if a = 1 then
-			  [cont_tac; snd_tac]
-		      	else
-			  [snd_tac; cont_tac] in
-		      Node(zz,"TACLIST",
-			   tacs1@(auxiliary_goals (h::clear_names)
-				   false "dummy" nprems))]))
-    | (str_list, int_list, nprems, c, []) 
-        when  (check_apply c (mk_db_indices int_list nprems)) &
-              (match c with Prod(_,_,_) -> false
-              |  _ -> true) &
-              (List.length int_list) + nprems > 0 ->
-          Some(add_clear_names_if_necessary
-	     (Node(zz,"Apply", [Node(zz,"COMMAND",[Nvar(zz, h)]);
-			     Node(zz,"BINDINGS", [])]))
-             clear_names)
-    | _ -> None)
-  | _ -> None;;
-*)
-
 let (head_tactic_patt: pbp_rule) = function
     avoid, clear_names, clear_flag, Some h, cstr, path, f ->
     (match down_prods (cstr, path, 0) with
@@ -652,11 +501,6 @@ let pbp_rules = ref [rem_cast;head_tactic_patt;forall_intro;imply_intro2;
 		      and_intro; or_intro; not_intro; ex_intro];;
 
 
-(* The tactic traced_try was intended to be used in tactics instead of
-   Try, with an argument  Node(zz, "TACTIC", [b]) where b is the tactic to
-   try.  However, the current design is not very robust to the fact that
-   Traced_Try may occur several times in the executed command! *)
-
 let try_trace = ref true;;
 
 let traced_try (f1:tactic) g =
@@ -670,24 +514,10 @@ let traced_try_entry = function
   |  _ -> failwith "traced_try_entry received wrong arguments";;
 
 
-let rec clean_trace flag =
-      function
-          Node(a,"Traced_Try", [Node(_,_,[b])]) ->
-             if flag then b else Node(zz,"Idtac",[])
-      	| Node(a,b,c) -> Node(a,b,List.map (clean_trace flag) c)
-        | t -> t;;
-
 (* When the recursive descent along the path is over, one includes the
    command requested by the point-and-shoot strategy.  Default is
    Try Assumption--Try Exact.  *)
 
-(*
-let default_ast optname constr path =
-      match optname with
-        None ->  Node(zz, "TRY", [Node(zz, "Assumption",[])])
-      | Some(a) -> Node(zz, "TRY", 
-                   [Node(zz, "Exact",[Node(zz,"COMMAND",[Nvar(zz,a)])])]);;
-*)
 
 let default_ast optname constr path = PbpThen [PbpTryAssumption optname]
 
@@ -710,100 +540,12 @@ let rec pbpt final_cmd avoid clear_names clear_flag opt_name constr path =
 (* these are the optimisation functions. *)
 (* This function takes care of flattening successive then commands. *)
 
-(*
-let rec optim1 =
-    function
-        Node(a,"TACTICLIST",b) ->
-          let tacs = List.map optim1 b in
-          let rec flatten = function
-            | [Node(a, "TACTICLIST", b')] ->
-                let rec last = function
-                    [] -> failwith "function last is called on an empty list"
-		  | [b] -> b
-		  | a::b -> last b in
-		(match last b' with
-		  Node(a, "TACLIST",_) -> [Node(a,"TACTICLIST", b')]
-		| _ -> flatten b')
-            | Node(a, "TACTICLIST", b')::others -> List.append (flatten b')
-                                                       (flatten others)
-            | Node(a, "Idtac",[])::others -> (flatten others)
-            | [Node(a, "TACLIST",tacs)] ->
-                 [Node(a, "TACLIST", List.map optim1 tacs)]
-            | t1::others -> t1::(flatten others)
-            | [] -> [] in
-          (match (flatten tacs) with
-            [] -> Node(zz,"Idtac", [])
-          | [t] -> t
-          | args -> Node(zz,"TACTICLIST", args))
-      |	t -> t;;
-*)
 
 (* Invariant: in [flatten_sequence t], occurrences of [PbpThenCont(l,t)] enjoy
     that t is some [PbpAtom t] *)
-(*
-let rec flatten_sequence =
-  function
-      PbpThens (tl1,tl2) -> PbpThens (tl1,List.map flatten_sequence tl2)
-    | PbpThen (tl1,t1) as x ->
-	(match flatten_sequence t1 with
-	  | PbpThenCont (tl2,t2) -> PbpThenCont (tl1@tl2,t2)
-	  | PbpThens (tl2,tl3) -> PbpThens (tl1@tl2,tl3)
-	  | PbpAtom _ -> x)
-    | PbpAtom t as x -> x;;
-*)
 
 (* This optimization function takes care of compacting successive Intro commands
    together. *)
-(*
-let rec optim2 =
-    function
-	Node(a,"TACTICLIST",b) ->
-         let get_ids = 
-           List.map (function Node(_,"IDENTIFIER", [Nvar(_,s)])->s
-             | Node(_,s,_) -> (failwith "unexpected node " ^ s)
-             |  _ -> failwith "get_ids expected an identifier") in
-         let put_ids ids =
-           Node(zz,"Intros",
-               	[Node(zz,"INTROPATTERN",
-		      [Node(zz,"LISTPATTERN", 
-			    List.map 
-			      (function s -> Node(zz,"IDENTIFIER",[Nvar(zz,s)]))
-			      ids)])]) in
-         let rec group_intros names = function
-             [] -> (match names with
-               [] -> []
-	     | l -> [put_ids l])
-           | Node(_,"Intros", 
-		  [Node(_,"INTROPATTERN",[Node(_,"LISTPATTERN", ids)])])::others ->
-		    group_intros (names@(get_ids ids)) others
-           | [Node(a,"TACLIST",b')] ->
-	       [Node(a,"TACLIST", List.map optim2 b')]
-           | t1::others -> 
-	       (match names with
-		 [] -> t1::(group_intros [] others)
-	       | l -> (put_ids l)::t1::(group_intros [] others)) in
-	 Node(a,"TACTICLIST",group_intros [] b)
-   | t -> t;;
-*)
-(*
-let rec optim2 = function
-  | TacThens (t,tl) -> TacThens (optim2 t, List.map optim2 tl)
-  | t ->
-      let get_ids = 
-	List.map (function IntroIdentifier _ as x -> x
-	  |  _ -> failwith "get_ids expected an identifier") in
-      let rec group_intros names = function
-	  [] -> (match names with
-              [] -> []
-	    | l -> [TacIntroPattern l])
-	| (TacIntroPattern ids)::others ->
-	    group_intros (names@(get_ids ids)) others
-	| t1::others -> 
-	    (match names with
-		[] -> t1::(group_intros [] others)
-	      | l -> (TacIntroPattern l)::t1::(group_intros [] others)) in
-      make_then (group_intros [] (flatten_sequence t))
-*)
 
 let rec group_intros names = function
     [] -> (match names with
@@ -819,37 +561,7 @@ let rec optim2 = function
   | PbpThens (tl1,tl2) -> PbpThens (group_intros [] tl1, List.map optim2 tl2)
   | PbpThen tl -> PbpThen (group_intros [] tl)
 
-(*
-let rec merge_ast_in_command com1 com2 =
-    let args1 =
-     (match com1 with
-	Node(_, "APPLIST", args) -> args
-     | _ -> failwith "unexpected com1 in merge_ast_in_command") in
-    let args2 =
-     (match com2 with
-        Node(_, "APPLIST", hyp::args) -> args
-     | _ -> failwith "unexpected com2 in merge_ast_in_command") in
-      Node(zz, "COMMAND", [Node(zz, "APPLIST", args1@args2)]);;
-*)
-(*
-let cleanup_clears empty_allowed names str_list other =
-  let rec clean_aux = function
-      [] -> []
-    | (Nvar(_,x) as fst_one)::tail ->
-      if List.mem x str_list then
-         clean_aux tail
-      else
-         fst_one::(clean_aux tail)
-    | _ -> failwith "unexpected argument in clean_aux" in
-  match clean_aux names with
-    [] -> (match other with 
-            [] -> 
-	      if empty_allowed then
-		[]
-	      else [Node(zz,"Idtac",[])]
-          | _ -> other)
-  | l -> Node(zz, "TRY", [Node(zz, "Clear", [Node(zz,"CLAUSE", l)])])::other;;
-*)
+
 let rec cleanup_clears str_list = function
     [] -> []
   | x::tail ->
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 1a6bfc4ca7..3e7cfd82a3 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -590,7 +590,7 @@ and fFORMULA = function
    fNODE "cofixc" 2
 | CT_elimc(x1, x2, x3, x4) ->
    fCASE x1;
-   fFORMULA x2;
+   fFORMULA_OPT x2;
    fFORMULA x3;
    fFORMULA_LIST x4;
    fNODE "elimc" 4
@@ -605,6 +605,12 @@ and fFORMULA = function
    fFORMULA x3;
    fFORMULA x4;
    fNODE "if" 4
+| CT_inductive_let(x1, x2, x3, x4) ->
+   fFORMULA_OPT x1;
+   fID_OPT_NE_LIST x2;
+   fFORMULA x3;
+   fFORMULA x4;
+   fNODE "inductive_let" 4
 | CT_int_encapsulator x -> fATOM "int_encapsulator";
    (f_atom_string x);
    print_string "\n"| CT_lambdac(x1, x2) ->
@@ -1257,8 +1263,8 @@ and fTACTIC_COM = function
    fNODE "superauto" 4
 | CT_symmetry -> fNODE "symmetry" 0
 | CT_tac_double(x1, x2) ->
-   fINT x1;
-   fINT x2;
+   fID_OR_INT x1;
+   fID_OR_INT x2;
    fNODE "tac_double" 2
 | CT_tacsolve(x,l) ->
    fTACTIC_COM x;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 3ac46fa7d9..2e791e8d5f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -5,7 +5,6 @@ open Char;;
 open Util;;
 open Ast;;
 open Names;;
-open Ctast;;
 open Ascent;;
 open Genarg;;
 open Rawterm;;
@@ -18,12 +17,6 @@ open Libnames;;
 
 let in_coq_ref = ref false;;
 
-let xlate_mut_stuff = ref ((fun _ -> 
-          Nvar((0,0), "function xlate_mut_stuff should not be used here")):
-              Ctast.t -> Ctast.t);;
-
-let set_xlate_mut_stuff v = xlate_mut_stuff := v;;
-
 let declare_in_coq () = in_coq_ref:=true;;
 
 let in_coq () = !in_coq_ref;;
@@ -168,18 +161,6 @@ let coerce_VARG_to_ID =
      x
     | _ -> xlate_error "coerce_VARG_to_ID";;
 
-let xlate_id =
- function
-    | Nvar (_, id) ->
-     (match id with
-     | "_" -> xlate_error "xlate_id: '_' is ident option"
-     | s -> CT_ident s)
-    | Id (_, id) ->
-     (match id with
-     | "_" -> xlate_error "xlate_id: '_' is ident option"
-     | s -> CT_ident s)
-    | _ -> xlate_error "xlate_id: not an identifier";;
-
 let xlate_id_unit = function
     None -> CT_unit
   | Some x -> CT_coerce_ID_to_ID_UNIT (xlate_ident x);;
@@ -189,11 +170,6 @@ let xlate_ident_opt =
     | None -> ctv_ID_OPT_NONE
     | Some id -> ctf_ID_OPT_SOME (xlate_ident id)
 
-let xlate_int =
- function
-    | Num (_, n) -> CT_int n
-    | _ -> xlate_error "xlate_int: not an int";;
-
 let xlate_id_to_id_or_int_opt s =
    CT_coerce_ID_OPT_to_ID_OR_INT_OPT
      (CT_coerce_ID_to_ID_OPT (CT_ident (string_of_id s)));;
@@ -210,11 +186,6 @@ let xlate_int_opt = function
   | Some n -> CT_coerce_INT_to_INT_OPT (CT_int n)
   | None ->  CT_coerce_NONE_to_INT_OPT CT_none
 
-let xlate_string =
- function
-    | Str (_, s) -> CT_string s
-    | _ -> xlate_error "xlate_string: not a string";;
-
 let tac_qualid_to_ct_ID ref = 
   CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref)))
 
@@ -240,16 +211,6 @@ let xlate_class = function
   | SortClass -> CT_ident "SORTCLASS"
   | RefClass qid -> loc_qualid_to_ct_ID qid
 
-let split_params =
- let rec sprec acc =
-  function
-     | (Id _ as p) :: l -> sprec (p::acc) l
-     | (Str _ as p) :: l -> sprec (p::acc) l
-     | (Num _ as p) :: l -> sprec (p::acc) l
-     | (Path _ as p) :: l -> sprec (p::acc) l
-     | l -> List.rev acc, l in
- sprec [];;
-
 let id_to_pattern_var ctid =
  match ctid with
  | CT_ident "_" -> 
@@ -261,14 +222,6 @@ let id_to_pattern_var ctid =
 
 exception Not_natural;;
 
-let rec nat_to_number =
- function
-    | Node (_, "APPLIST", ((Nvar (_, "S")) :: (v :: []) as v0)) ->
-     1 + nat_to_number v
-    | Nvar (_, "O") -> 0
-    | _ -> raise Not_natural;;
-
-
 let xlate_sort =
   function
     | RProp Term.Pos -> CT_sortc "Set"
@@ -291,8 +244,9 @@ let xlate_reference = function
 let rec xlate_match_pattern =
  function
    | CPatAtom(_, Some s) -> id_to_pattern_var (xlate_reference  s)
-   |CPatAtom(_, None) -> id_to_pattern_var (CT_ident "_")
-   |  CPatCstr (_, f1 , (arg1 :: args)) ->
+   | CPatAtom(_, None) -> id_to_pattern_var (CT_ident "_")
+   | CPatCstr(_, f, []) -> id_to_pattern_var (xlate_reference f)
+   | CPatCstr (_, f1 , (arg1 :: args)) ->
      CT_pattern_app
       (id_to_pattern_var (xlate_reference  f1),
       CT_match_pattern_ne_list
@@ -301,7 +255,9 @@ let rec xlate_match_pattern =
     | CPatAlias  (_,  pattern, id) ->
      CT_pattern_as
       (xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id))
-    | _ -> xlate_error "Unexpected data while translating a pattern";;
+    | CPatDelimiters(_, _, _) -> xlate_error "CPatDelimitors"
+    | CPatNumeral(_,_) -> xlate_error "CPatNumeral";;
+
 
 
 
@@ -340,6 +296,8 @@ and
 and 
   xlate_binder_list = function
   l -> CT_binder_list( List.map xlate_binder_l l)
+and  cvt_fixpoint_binders bl =
+  CT_binder_list(List.map xlate_binder bl)
 and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 
      CRef r -> varc (xlate_reference r)
@@ -361,19 +319,49 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) -> 
 		   CT_if(xlate_formula_opt po,
                    xlate_formula c,xlate_formula b1,xlate_formula b2)		
-
+   | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) ->
+       CT_inductive_let(xlate_formula_opt po,
+	       xlate_id_opt_ne_list l,
+	       xlate_formula c, xlate_formula b) 
+   | COrderedCase (_,c,v,e,l) -> 
+       let case_string = match c with
+	   Term.MatchStyle -> "Match"
+	 | _ -> "Case" in
+	 CT_elimc(CT_case "Case", xlate_formula_opt v, xlate_formula e,
+		  CT_formula_list(List.map xlate_formula l))
    | CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
    | CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l)
    | CNumeral(_, i) -> CT_int_encapsulator(Bignat.bigint_to_string i)
    | CHole _ -> CT_existvarc 
-   | COrderedCase (_,_,_,_,_) -> xlate_error "TODO:COrderedCase"
    | CDynamic (_, _) -> xlate_error "TODO:CDynamic"
    | CDelimiters (_, key, num) -> CT_num_encapsulator(CT_num_type key , xlate_formula  num)
-   | CCast (_, _, _) -> xlate_error "TODO:CCast"
-   | CMeta (_, _) -> xlate_error "TODO:CMeta"
-   | CCoFix (_, _, _) -> xlate_error "TODO:CCoFix"
-   | CFix (_, _, _) -> xlate_error "TODO:CFix"
-
+   | CCast (_, e, t) -> 
+       CT_coerce_TYPED_FORMULA_to_FORMULA
+	 (CT_typed_formula(xlate_formula e, xlate_formula t))
+   | CMeta (_, i) -> CT_coerce_ID_to_FORMULA(CT_metac (CT_int i))
+   | CCoFix (_, (_, id), lm::lmi) -> 
+     let strip_mutcorec (fid, arf, ardef) =
+	CT_cofix_rec (xlate_ident fid, xlate_formula arf, xlate_formula ardef) in
+        CT_cofixc(xlate_ident id,
+	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
+   | CFix (_, (_, id), lm::lmi) ->       
+     let strip_mutrec (fid, n, arf, ardef) =
+        let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
+        let arf = xlate_formula arf in
+        let ardef = xlate_formula ardef in
+	match cvt_fixpoint_binders bl with
+	  | CT_binder_list (b :: bl) ->
+	      CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
+                arf, ardef)
+          | _ -> xlate_error "mutual recursive" in
+       CT_fixc (xlate_ident id, 
+         	CT_fix_binder_list
+		  (CT_coerce_FIX_REC_to_FIX_BINDER 
+		     (strip_mutrec lm), List.map 
+		       (fun x-> CT_coerce_FIX_REC_to_FIX_BINDER (strip_mutrec x))
+		       lmi)) 
+   | CCoFix _ -> assert false
+   | CFix _ -> assert false
 and xlate_formula_expl = function
     (a, None) -> xlate_formula a
   | (a, i) -> CT_bang(xlate_int_opt i, xlate_formula a)
@@ -519,17 +507,6 @@ let is_tactic_special_case = function
     "AutoRewrite" -> true
   | _ -> false;;
 
-let tactic_special_case cont_function cvt_arg = function
-    "AutoRewrite", (tac::v::bl) ->
-      CT_autorewrite
-	(CT_id_ne_list(xlate_id v, List.map xlate_id bl),
-	   CT_coerce_TACTIC_COM_to_TACTIC_OPT(cont_function tac))
-  | "AutoRewrite", (v::bl) ->
-      CT_autorewrite
-	(CT_id_ne_list(xlate_id v, List.map xlate_id bl),
-	 CT_coerce_NONE_to_TACTIC_OPT CT_none)
-  | _ -> assert false;;
-	      
 let xlate_context_pattern = function
   | Term v -> 
       CT_coerce_FORMULA_to_CONTEXT_PATTERN (xlate_formula v)
@@ -703,9 +680,8 @@ and xlate_tac =
     | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
     | TacChange (_, f, b) -> xlate_error "TODO: Change subterms"
     | TacExtend (_,"Contradiction",[]) -> CT_contradiction
-    | TacDoubleInduction (AnonHyp n1, AnonHyp n2) ->
-	CT_tac_double (CT_int n1, CT_int n2)
-    | TacDoubleInduction _ -> xlate_error "TODO: Double Induction id1 id2"
+    | TacDoubleInduction (n1, n2) ->
+	CT_tac_double (xlate_quantified_hypothesis n1, xlate_quantified_hypothesis n2)
     | TacExtend (_,"Discriminate", [idopt]) ->
      CT_discriminate_eq
          (xlate_quantified_hypothesis_opt
@@ -1146,30 +1122,6 @@ let build_record_field_list l =
       xlate_error "TODO: manifest fields in Record" in
  CT_recconstr_list (List.map build_record_field l);;
 
-let xlate_ast =
- let rec xlate_ast_aux =
-  function
-     | Node (_, s, tl) ->
-      CT_astnode (CT_ident s, CT_ast_list (List.map xlate_ast_aux tl))
-     | Nvar (_, s) ->
-      CT_coerce_ID_OR_STRING_to_AST
-       (CT_coerce_STRING_to_ID_OR_STRING (CT_string s))
-     | Slam (_, (Some s), t) ->
-      CT_astslam (CT_coerce_ID_to_ID_OPT (CT_ident s), xlate_ast_aux t)
-     | Slam (_, None, t) -> CT_astslam (ctv_ID_OPT_NONE, xlate_ast_aux t)
-     | Num (_, i) -> failwith "Numbers not treated in xlate_ast"
-     | Id (_, s) ->
-      CT_coerce_ID_OR_STRING_to_AST
-       (CT_coerce_STRING_to_ID_OR_STRING (CT_string s))
-     | Str (_, s) ->
-      CT_coerce_ID_OR_STRING_to_AST
-       (CT_coerce_STRING_to_ID_OR_STRING (CT_string s))
-     | Dynamic(_,_) -> failwith "Dynamics not treated in xlate_ast"
-     | Path (_, sl) ->
-      CT_astpath
-       (CT_id_list (List.map (function s -> CT_ident s) sl)) in
- xlate_ast_aux;;
-
 let get_require_flags impexp spec =
  let ct_impexp =
   match impexp with
@@ -1198,8 +1150,7 @@ let cvt_vernac_binder = function
 let cvt_vernac_binders args =
   CT_binder_list(List.map cvt_vernac_binder args)
 
-let cvt_fixpoint_binders bl =
-  CT_binder_list(List.map xlate_binder bl)
+
 
 let xlate_comment = function
     CommentConstr c -> CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula c)
diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli
index 6109816b5c..bedb4ac82b 100644
--- a/contrib/interface/xlate.mli
+++ b/contrib/interface/xlate.mli
@@ -3,10 +3,7 @@ open Ascent;;
 val xlate_vernac : Vernacexpr.vernac_expr -> ct_COMMAND;;
 val xlate_tactic : Tacexpr.raw_tactic_expr -> ct_TACTIC_COM;;
 val xlate_formula : Topconstr.constr_expr -> ct_FORMULA;;
-val xlate_int : Ctast.t -> ct_INT;;
-val xlate_string : Ctast.t -> ct_STRING;;
 val xlate_ident : Names.identifier -> ct_ID;;
 val xlate_vernac_list : Vernacexpr.vernac_expr -> ct_COMMAND_LIST;;
 
-val set_xlate_mut_stuff : (Ctast.t -> Ctast.t) -> unit;;
 val declare_in_coq : (unit -> unit);;