diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-23 18:51:11 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-23 18:51:11 +0000 |
| commit | 7e02b97b3017a5a3055fca8e0fc6e89f84b6a1c4 (patch) | |
| tree | 1009560f396c397caa537471fc922aa0fb2af0bf /tactics/tacinterp.ml | |
| parent | e3567014035a55cfde44099ce59d142d084faac5 (diff) | |
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
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index db6a45e1e..1dc0f6589 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 |