remove undocumented and scarcely-used tactic auto decomp

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

3 files changed, 7 insertions, 87 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index cedec80a17..8b4f5eb611 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1405,51 +1405,23 @@ let decomp_empty_term dbg (id,_,typc) gl =
 let extend_local_db gl decl db =
   Hint_db.add_list (make_resolve_hyp (pf_env gl) (project gl) decl) db
 
-(* Try to decompose hypothesis [decl] into atomic components of a
-   conjunction with maximum depth [p] (or solve the goal from an
-   empty type) then call the continuation tactic with hint db extended
-   with the obtained not-further-decomposable hypotheses *)
-
-let rec decomp_and_register_decl dbg p kont (id,_,_ as decl) db gl =
-  if p = 0 then
-    kont (extend_local_db gl decl db) gl
-  else
-    tclORELSE0
-      (decomp_empty_term dbg decl)
-      (decomp_unary_term_then dbg decl (intros_decomp dbg (p-1) kont [] db)
-	(kont (extend_local_db gl decl db))) gl
-
-(* Introduce [n] hypotheses, then decompose then with maximum depth [p] and
-   call the continuation tactic [kont] with the hint db extended
-   with the so-obtained not-further-decomposable hypotheses *)
-
-and intros_decomp dbg p kont decls db n =
-  if n = 0 then
-    decomp_and_register_decls dbg p kont decls db
-  else
-    tclTHEN (dbg_intro dbg) (onLastDecl (fun d ->
-      (intros_decomp dbg p kont (d::decls) db (n-1))))
-
-(* Decompose hypotheses [hyps] with maximum depth [p] and
-   call the continuation tactic [kont] with the hint db extended
-   with the so-obtained not-further-decomposable hypotheses *)
-
-and decomp_and_register_decls dbg p kont decls =
-  List.fold_left (decomp_and_register_decl dbg p) kont decls
+(* Introduce an hypothesis, then call the continuation tactic [kont]
+   with the hint db extended with the so-obtained hypothesis *)
 
+let intro_register dbg kont db =
+  tclTHEN (dbg_intro dbg)
+    (onLastDecl (fun decl gl -> kont (extend_local_db gl decl db) gl))
 
-(* decomp is an natural number giving an indication on decomposition
-   of conjunction in hypotheses, 0 corresponds to no decomposition *)
 (* n is the max depth of search *)
 (* local_db contains the local Hypotheses *)
 
 exception Uplift of tactic list
 
-let search_gen d p n mod_delta db_list local_db =
+let search d n mod_delta db_list local_db =
   let rec search d n local_db =
     if n=0 then (fun gl -> error "BOUND 2") else
       tclORELSE0 (dbg_assumption d)
-	(tclORELSE0 (intros_decomp d p (search d n) [] local_db 1)
+	(tclORELSE0 (intro_register d (search d n) local_db)
 	   (fun gl ->
 	     let d' = incr_dbg d in
 	     tclFIRST
@@ -1459,8 +1431,6 @@ let search_gen d p n mod_delta db_list local_db =
   in
   search d n local_db
 
-let search dbg = search_gen dbg 0
-
 let default_search_depth = ref 5
 
 let delta_auto ?(debug=Off) mod_delta n lems dbnames gl =
@@ -1499,35 +1469,3 @@ let inj_or_var = Option.map (fun n -> ArgArg n)
 let h_auto ?(debug=Off) n lems l =
   Refiner.abstract_tactic (TacAuto (debug,inj_or_var n,List.map snd lems,l))
     (gen_auto ~debug n lems l)
-
-(**************************************************************************)
-(*                  The "destructing Auto" from Eduardo                   *)
-(**************************************************************************)
-
-(* Depth of search after decomposition of hypothesis, by default
-   one look for an immediate solution *)
-let default_search_decomp = ref 20
-
-let destruct_auto d p lems n gl =
-  decomp_and_register_decls d p (fun local_db gl ->
-    search_gen d p n false (List.map searchtable_map ["core";"extcore"])
-      (add_hint_lemmas false lems local_db gl) gl)
-    (pf_hyps gl)
-    (Hint_db.empty empty_transparent_state false)
-    gl
-
-let dautomatic ?(debug=Off) des_opt lems n =
-  let d = mk_auto_dbg debug in
-  tclTRY_dbg d (destruct_auto d des_opt lems n)
-
-let dauto ?(debug=Off) (n,p) lems =
-  let p = match p with Some p -> p | None -> !default_search_decomp in
-  let n = match n with Some n -> n | None -> !default_search_depth in
-  dautomatic ~debug p lems n
-
-let default_dauto = dauto (None,None) []
-
-let h_dauto ?(debug=Off) (n,p) lems =
-  Refiner.abstract_tactic
-    (TacDAuto (debug,inj_or_var n,p,List.map snd lems))
-    (dauto ~debug (n,p) lems)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 69a526e5ae..49a7ef3055 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -264,17 +264,6 @@ val h_trivial : ?debug:Tacexpr.debug ->
 
 val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds
 
-(** Destructing Auto *)
-
-(** DAuto *)
-val dauto :  ?debug:Tacexpr.debug ->
-  int option * int option -> open_constr list -> tactic
-val default_search_decomp : int ref
-val default_dauto : tactic
-
-val h_dauto : ?debug:Tacexpr.debug ->
-  int option * int option -> open_constr list -> tactic
-
 (** Hook for changing the initialization of auto *)
 
 val add_auto_init : (unit -> unit) -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index db6a45e1e6..1dc0f6589b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -718,9 +718,6 @@ let rec intern_atomic lf ist x =
   | TacAuto (d,n,lems,l) ->
       TacAuto (d,Option.map (intern_or_var ist) n,
         List.map (intern_constr ist) lems,l)
-  | TacDAuto (d,n,p,lems) ->
-      TacDAuto (d,Option.map (intern_or_var ist) n,p,
-        List.map (intern_constr ist) lems)
 
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct (isrec,h) ->
@@ -2413,9 +2410,6 @@ and interp_atomic ist gl tac =
       Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
 	(interp_auto_lemmas ist env sigma lems)
 	(Option.map (List.map (interp_hint_base ist)) l)
-  | TacDAuto (debug,n,p,lems) ->
-      Auto.h_dauto ~debug (Option.map (interp_int_or_var ist) n,p)
-      (interp_auto_lemmas ist env sigma lems)
 
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct (isrec,h) ->
@@ -2855,7 +2849,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Automation tactics *)
   | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l)
   | TacAuto (d,n,lems,l) -> TacAuto (d,n,List.map (subst_glob_constr subst) lems,l)
-  | TacDAuto (d,n,p,lems) -> TacDAuto (d,n,p,List.map (subst_glob_constr subst) lems)
 
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct (isrec,h) as x -> x