suppression de newtauto

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

4 files changed, 79 insertions, 347 deletions

diff --git a/.depend b/.depend
index 21377c152e..2a138ce2b4 100644
--- a/.depend
+++ b/.depend
@@ -45,10 +45,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/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/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.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 
@@ -68,9 +68,6 @@ 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 \
@@ -99,6 +96,9 @@ library/library.cmi: library/libnames.cmi library/libobject.cmi \
 library/nameops.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
     lib/util.cmi 
+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 
@@ -318,11 +318,11 @@ 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 
 translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \
     parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
     kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
@@ -340,11 +340,11 @@ 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 
@@ -491,6 +491,14 @@ ide/config_lexer.cmo: ide/config_parser.cmi lib/util.cmi
 ide/config_lexer.cmx: ide/config_parser.cmx lib/util.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: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
+    ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
+    ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi ide/undo.cmi \
+    lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi 
+ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
+    ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
+    ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx ide/undo.cmx \
+    lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi 
 ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
     kernel/declarations.cmi kernel/environ.cmi pretyping/evarutil.cmi \
     pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \
@@ -513,14 +521,6 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
     toplevel/vernacentries.cmx toplevel/vernacexpr.cmx ide/coq.cmi 
 ide/coq_tactics.cmo: ide/coq_tactics.cmi 
 ide/coq_tactics.cmx: ide/coq_tactics.cmi 
-ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
-    ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
-    ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi ide/undo.cmi \
-    lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi 
-ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
-    ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
-    ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx ide/undo.cmx \
-    lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi 
 ide/find_phrase.cmo: ide/ideutils.cmi 
 ide/find_phrase.cmx: ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmi 
@@ -671,6 +671,12 @@ 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 \
@@ -679,12 +685,6 @@ 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/options.cmi lib/pp.cmi \
     lib/predicate.cmi lib/util.cmi kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/options.cmx lib/pp.cmx \
@@ -765,10 +765,10 @@ 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/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/gmap.cmo: lib/gmap.cmi 
+lib/gmap.cmx: lib/gmap.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
@@ -777,24 +777,14 @@ 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.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/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
+lib/pp.cmx: lib/pp_control.cmx lib/pp.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 \
@@ -899,6 +889,16 @@ 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 
@@ -1865,26 +1865,6 @@ tactics/nbtermdn.cmo: tactics/btermdn.cmi lib/gmap.cmi library/libobject.cmi \
 tactics/nbtermdn.cmx: tactics/btermdn.cmx lib/gmap.cmx library/libobject.cmx \
     library/library.cmx kernel/names.cmx pretyping/pattern.cmx \
     kernel/term.cmx tactics/termdn.cmx lib/util.cmx tactics/nbtermdn.cmi 
-tactics/newtauto.cmo: parsing/ast.cmi toplevel/cerrors.cmi parsing/coqast.cmi \
-    kernel/declarations.cmi parsing/egrammar.cmi kernel/environ.cmi \
-    pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
-    tactics/hipattern.cmi pretyping/inductiveops.cmi library/libnames.cmi \
-    kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
-    parsing/printer.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
-    proofs/refiner.cmi kernel/sign.cmi proofs/tacexpr.cmo \
-    tactics/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
-    tactics/tactics.cmi tactics/tauto.cmo kernel/term.cmi \
-    pretyping/termops.cmi interp/topconstr.cmi lib/util.cmi 
-tactics/newtauto.cmx: parsing/ast.cmx toplevel/cerrors.cmx parsing/coqast.cmx \
-    kernel/declarations.cmx parsing/egrammar.cmx kernel/environ.cmx \
-    pretyping/evd.cmx interp/genarg.cmx library/global.cmx \
-    tactics/hipattern.cmx pretyping/inductiveops.cmx library/libnames.cmx \
-    kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
-    parsing/printer.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \
-    proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx \
-    tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
-    tactics/tactics.cmx tactics/tauto.cmx kernel/term.cmx \
-    pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx 
 tactics/refine.cmo: proofs/clenv.cmi kernel/environ.cmi pretyping/evd.cmi \
     kernel/names.cmi lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi \
     pretyping/retyping.cmi kernel/sign.cmi proofs/tacmach.cmi \
@@ -2023,10 +2003,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/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/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
+tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.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 \
@@ -2233,18 +2213,6 @@ 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: interp/constrextern.cmi interp/constrintern.cmi \
-    parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
-    kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
-    lib/pp.cmi translate/ppvernacnew.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: interp/constrextern.cmx interp/constrintern.cmx \
-    parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
-    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
-    lib/pp.cmx translate/ppvernacnew.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 \
@@ -2305,6 +2273,18 @@ 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: interp/constrextern.cmi interp/constrintern.cmi \
+    parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
+    kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmi translate/ppvernacnew.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: interp/constrextern.cmx interp/constrintern.cmx \
+    parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
+    kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
+    lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx lib/system.cmx \
+    lib/util.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \
     interp/constrextern.cmi interp/constrintern.cmi parsing/coqast.cmi \
     pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -2381,6 +2361,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.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 \
@@ -2397,18 +2389,6 @@ 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 \
@@ -3083,6 +3063,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.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 \
@@ -3107,14 +3095,6 @@ 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 \
@@ -3345,12 +3325,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 \
@@ -3405,8 +3385,6 @@ 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 \
@@ -3431,10 +3409,8 @@ contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
 contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
     lib/util.cmx toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx 
-ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
-    ide/utils/configwin_types.cmo ide/utils/configwin.cmi 
-ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
-    ide/utils/configwin_types.cmx ide/utils/configwin.cmi 
+contrib/xml/xml.cmo: contrib/xml/xml.cmi 
+contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 ide/utils/configwin_html_config.cmo: ide/utils/configwin_ihm.cmo \
     ide/utils/configwin_messages.cmo ide/utils/configwin_types.cmo \
     ide/utils/uoptions.cmi 
@@ -3445,6 +3421,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/configwin_messages.cmo \
     ide/utils/configwin_types.cmo ide/utils/okey.cmi ide/utils/uoptions.cmi 
 ide/utils/configwin_ihm.cmx: ide/utils/configwin_messages.cmx \
     ide/utils/configwin_types.cmx ide/utils/okey.cmx ide/utils/uoptions.cmx 
+ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
+    ide/utils/configwin_types.cmo ide/utils/configwin.cmi 
+ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
+    ide/utils/configwin_types.cmx ide/utils/configwin.cmi 
 ide/utils/configwin_types.cmo: ide/utils/configwin_keys.cmo \
     ide/utils/uoptions.cmi 
 ide/utils/configwin_types.cmx: ide/utils/configwin_keys.cmx \
@@ -3455,8 +3435,6 @@ ide/utils/uoptions.cmo: ide/utils/uoptions.cmi
 ide/utils/uoptions.cmx: ide/utils/uoptions.cmi 
 tactics/tauto.cmo: parsing/grammar.cma
 tactics/tauto.cmx: parsing/grammar.cma
-tactics/newtauto.cmo: parsing/grammar.cma
-tactics/newtauto.cmx: parsing/grammar.cma
 tactics/eqdecide.cmo: parsing/grammar.cma
 tactics/eqdecide.cmx: parsing/grammar.cma
 tactics/extraargs.cmo: parsing/grammar.cma
diff --git a/.depend.camlp4 b/.depend.camlp4
index 77b3b80925..13318ae601 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -1,5 +1,4 @@
 tactics/tauto.ml: parsing/grammar.cma
-tactics/newtauto.ml: parsing/grammar.cma
 tactics/eqdecide.ml: parsing/grammar.cma
 tactics/extraargs.ml: parsing/grammar.cma
 tactics/extratactics.ml: parsing/grammar.cma
diff --git a/Makefile b/Makefile
index 83c45e98d7..178abf1334 100644
--- a/Makefile
+++ b/Makefile
@@ -188,7 +188,7 @@ parsing/q_tactic.ml4: parsing/g_tactic.ml4
 parsing/q_ltac.ml4: parsing/g_ltac.ml4
 	camlp4o -I parsing grammar.cma pa_ifdef.cmo pa_extend.cmo pr_o.cmo pr_extend.cmo -quotify -DQuotify -o parsing/q_ltac.ml4 -impl parsing/g_ltac.ml4
 
-SPECTAC= tactics/tauto.ml4 tactics/newtauto.ml4 tactics/eqdecide.ml4
+SPECTAC= tactics/tauto.ml4 tactics/eqdecide.ml4
 USERTAC = $(SPECTAC)
 ML4FILES += $(USERTAC) tactics/extraargs.ml4 tactics/extratactics.ml4 \
 	tactics/eauto.ml4 
diff --git a/tactics/newtauto.ml4 b/tactics/newtauto.ml4
deleted file mode 100644
index 0c8f9bb4af..0000000000
--- a/tactics/newtauto.ml4
+++ /dev/null
@@ -1,245 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
-(*i $Id$ i*)
-
-open Ast
-open Coqast
-open Hipattern
-open Names
-open Libnames
-open Pp
-open Proof_type
-open Tacticals
-open Tacinterp
-open Tactics
-open Tacexpr
-open Util
-open Term
-open Termops
-open Declarations
-
-let myprint env rc t=
-	let env2=Environ.push_rel_context rc env in
-	let ppstr=Printer.prterm_env env2 t in
-	Pp.msgnl ppstr
-
-let tacinj tac=valueIn (VTactic (dummy_loc,tac))
-
-let tclATMOSTn n tac1 gl=
-  let result=tac1 gl in
-    if List.length (fst result).it <= n then result
-    else (tclFAIL 0 "Not enough subgoals" gl)
-
-let tclTRY_REV_HYPS (tac : constr->tactic) gl = 
-  tclTRY_sign tac (List.rev (Tacmach.pf_hyps gl)) gl
- 
-let rec nb_prod_after n c=
-  match kind_of_term c with
-    | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else 
-	1+(nb_prod_after 0 b)
-    | _            -> 0
-
-let nhyps ind = 
-  let (mib,mip) = Global.lookup_inductive ind in
-  let constr_types = mip.mind_nf_lc in 
-  let nhyps = nb_prod_after mip.mind_nparams in	
-    Array.map nhyps constr_types
-
-let isrec ind=
-  let (mib,mip) = Global.lookup_inductive ind in
-  Inductiveops.mis_is_recursive (ind,mib,mip)
-
-let simplif=Tauto.reduction_not_iff
-
-let rule_axiom=assumption
-		      
-let rule_rforall tac=tclTHEN intro tac
-
-let rule_rarrow=interp  <:tactic<Match Reverse Context With
-      | [|- ?1 -> ?2 ] -> Intro>>
-
-let rule_larrow= 
-  (interp <:tactic<(Match Reverse Context With 
-			    [f:?1->?2;x:?1|-?] ->
-			      Generalize (f x);Clear f;Intro)>>)
-
-let rule_simp_larrow tac=
-  let itac=tacinj tac in
-  (interp <:tactic<(Match Reverse Context With 
-			    [f:?1->?2|-?] ->
-			      Assert ?1;[Solve $itac|IdTac])>>)
-
-
-let rule_named_llarrow id gl=
-    (try let nam=destVar id in
-    let body=Tacmach.pf_get_hyp_typ gl nam in
-    let (_,cc,c)=destProd body in
-    if dependent (mkRel 1) c then tclFAIL 0 "" else
-    let (_,ta,b)=destProd cc in
-    if dependent (mkRel 1) b then tclFAIL 0 "" else 
-    let tb=pop b and tc=pop c in
-    let d=mkLambda (Anonymous,tb,
-    mkApp (id,[|mkLambda (Anonymous,(lift 1 ta),(mkRel 2))|])) in
-    let env=Tacmach.pf_env gl in
-      tclTHENS (cut tc)
-	[tclTHEN intro (clear [nam]);
-	 tclTHENS (cut cc) 
-	   [exact_check id; tclTHENLIST [generalize [d];intro;clear [nam]]]]
-   with Invalid_argument _ -> tclFAIL 0 "") gl
-
-let rule_llarrow tac=
-  tclTRY_REV_HYPS 
-    (fun id->tclTHENS (rule_named_llarrow id) [tclIDTAC;tac])
-		       (* this rule always increases the number of goals*)
-
-let rule_rind tac gl=
-  (let (hdapp,args)=decompose_app gl.it.Evd.evar_concl in
-     try let ind=destInd hdapp in
-       if isrec ind then tclFAIL 0 "Found a recursive inductive type" else
-	 any_constructor (Some tac)
-     with Invalid_argument _ -> tclFAIL 0 "") gl 
-  
-let rule_rind_rev (* b *) gl=  
-  (let (hdapp,args)=decompose_app gl.it.Evd.evar_concl in
-     try let ind=destInd hdapp in
-       if (isrec ind)(* || (not b && (nhyps ind).(0)>1) *) then
-	 tclFAIL 0 "Found a recursive inductive type"
-       else
-	 simplest_split
-     with Invalid_argument _ -> tclFAIL 0 "") gl 
-  (* this rule increases the number of goals 
-if the unique constructor has several hyps.
-i.e if (nhyps ind).(0)>1 *)
-
-let rule_named_false id gl=
-  (try let nam=destVar id in
-   let body=Tacmach.pf_get_hyp_typ gl nam in
-     if is_empty_type body then (simplest_elim id)
-     else tclFAIL 0 "Found an non empty type"
-   with Invalid_argument _ -> tclFAIL 0 "") gl
-
-let rule_false=tclTRY_REV_HYPS rule_named_false
-
-let rule_named_lind (*b*) id gl= 
-  (try let nam=destVar id in
-   let body=Tacmach.pf_get_hyp_typ gl nam in
-   let (hdapp,args) = decompose_app body in
-   let ind=destInd hdapp in
-   (*let nconstr=
-    if b then 0 else 
-      Array.length (snd (Global.lookup_inductive ind)).mind_consnames in *)
-     if (isrec ind) (*|| (nconstr>1)*) then 
-       tclFAIL 0 "Found a recursive inductive type"
-     else 
-       let l=nhyps ind in
-       let f n= tclDO n intro in
-	 tclTHENSV (tclTHEN (simplest_elim id) (clear [nam])) (Array.map f l)
-   with Invalid_argument _ -> tclFAIL 0 "") gl
-  
-let rule_lind (* b *) =
-  tclTRY_REV_HYPS (rule_named_lind (* b *))
-(* number of goals increases if ind has several constructors *)
-
-let rule_named_llind id gl= 
-    (try let nam=destVar id in 
-    let body=Tacmach.pf_get_hyp_typ gl nam in
-    let (_,xind,b) =destProd body in
-    if dependent (mkRel 1) b then tclFAIL 0 "Found a dependent product" else  
-    let (hdapp,args) = decompose_app xind in
-    let vargs=Array.of_list args in
-    let ind=destInd hdapp in
-    if isrec ind then tclFAIL 0 "" else
-    let (mib,mip) = Global.lookup_inductive ind in
-    let n=mip.mind_nparams in
-    if n<>(List.length args) then tclFAIL 0 "" else
-    let p=nhyps ind in
-    let types= mip.mind_nf_lc in
-    let names= mip.mind_consnames in
-
-	(* construire le terme  H->B, le generaliser etc *)   
-    let myterm i=
-	let env=Tacmach.pf_env gl and emap=Tacmach.project gl in
-	let t1=Reductionops.hnf_prod_appvect env emap types.(i) vargs in
-	let (rc,_)=Sign.decompose_prod_n_assum p.(i) t1 in
-	let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in
-	let vars=Array.init p.(i) (fun j->mkRel (p.(i)-j)) in
-	let capply=mkApp ((lift p.(i) cstr),vars) in
-	let head=mkApp ((lift p.(i) id),[|capply|]) in
-	Sign.it_mkLambda_or_LetIn head rc in
-	
-    let newhyps=List.map myterm (interval 0 ((Array.length p)-1)) in
-     tclTHEN (generalize newhyps)
-	(tclTHEN (clear [nam]) (tclDO (Array.length p) intro))
-	with Invalid_argument _ ->tclFAIL 0 "") gl
-
-let rule_llind=tclTRY_REV_HYPS rule_named_llind
-
-let default_stac = interp(<:tactic< Auto with * >>)
-
-let rec newtauto b stac gl=
-  let wrap tac=if b then tac else 
-    tclATMOSTn 1 (tclTHEN tac (tclSOLVE [stac])) in
-    (tclTHEN simplif 
-       (tclORELSE 
-	  (tclTHEN 
-	     (tclFIRST [
-		rule_axiom;
-		rule_false;
-		rule_rarrow;
-		wrap rule_lind; 
-		rule_larrow;
-		rule_llind;
-		wrap rule_rind_rev; 
-		rule_llarrow (tclSOLVE [newtauto b stac]);
-		rule_rind (tclSOLVE [newtauto b stac]);
-		rule_rforall (tclSOLVE [newtauto b stac]);
-		if b then tclFAIL 0 "" else (rule_simp_larrow stac)])
-		(tclPROGRESS (newtauto b stac)))
-		stac)) gl
- 
-let q_elim tac=
-  let vtac=Tacexpr.TacArg (valueIn (VTactic (dummy_loc,tac))) in	
-  interp <:tactic<
-  Match Context With 
-    [x:?1;H:?1->?|-?]->
-      Generalize (H x);Clear H;$vtac>>
-
-let rec lfo n=
-  if n=0 then (tclFAIL 0 "NewLinearIntuition failed") else
-    let p=if n<0 then n else (n-1) in
-    let lfo_rec=q_elim (fun gl->lfo p gl) in
-      newtauto true lfo_rec
-
-let lfo_wrap n gl= 
-  try lfo n gl
-  with
-    Refiner.FailError _ | UserError _ ->
-      errorlabstrm "NewLinearIntuition" [< str "NewLinearIntuition failed." >]
-
-TACTIC EXTEND NewIntuition
-      [ "NewIntuition" ] -> [ newtauto true default_stac ]
-      |[ "NewIntuition" tactic(t)] -> [ newtauto true (snd t) ]
-END
-
-TACTIC EXTEND Intuition1
-      [ "Intuition1" ] -> [ newtauto false default_stac ]
-      |[ "Intuition1" tactic(t)] -> [ newtauto false (snd t) ]
-END
-
-TACTIC EXTEND NewTauto
-  [ "NewTauto" ] -> [ newtauto true (tclFAIL 0 "NewTauto failed") ]
-END
-
-TACTIC EXTEND NewLinearIntuition
-  [ "NewLinearIntuition" ] -> [ lfo_wrap (-1) ]
-|  [ "NewLinearIntuition" integer(n)] -> [ lfo_wrap n ]
-END
-