diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-29 11:20:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-29 13:24:45 +0100 |
| commit | 7dd8c2bf4747c94be6f18d7fdd0e3b593f560a2f (patch) | |
| tree | 31301a44d27401d5fad006c9b400c9dd8f0d4d16 /tactics | |
| parent | d0bc16d1a0626f4137797bbf0c91e972a0ff43ac (diff) | |
Moving the "clearbody" tactic to TACTIC EXTEND.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/coretactics.ml4 | 6 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 9 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 1 |
4 files changed, 6 insertions, 11 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index ab97dad70..b68aab621 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -216,6 +216,12 @@ TACTIC EXTEND clear | [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ] END +(* Clearbody *) + +TACTIC EXTEND clearbody + [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ] +END + (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) open Tacexpr diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index bea8d3469..9775f103f 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -525,7 +525,6 @@ let rec intern_atomic lf ist x = let h2 = intern_quantified_hypothesis ist h2 in TacDoubleInduction (h1,h2) (* Context management *) - | TacClearBody l -> TacClearBody (List.map (intern_hyp ist) l) | TacMove (id1,id2) -> TacMove (intern_hyp ist id1,intern_move_location ist id2) | TacRename l -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 74121d3ab..b2f539fb9 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1881,15 +1881,6 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacDoubleInduction (h1,h2)) (Elim.h_double_induction h1 h2) (* Context management *) - | TacClearBody l -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = pf_env gl in - let sigma = project gl in - let l = interp_hyp_list ist env sigma l in - name_atomic ~env - (TacClearBody l) - (Tactics.clear_body l) - end } | TacMove (id1,id2) -> Proofview.Goal.enter { enter = begin fun gl -> Proofview.V82.tactic (Tactics.move_hyp (interp_hyp ist (pf_env gl) (project gl) id1) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 0b8dbb6e3..50730eaea 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -167,7 +167,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacDoubleInduction (h1,h2) as x -> x (* Context management *) - | TacClearBody l as x -> x | TacMove (id1,id2) as x -> x | TacRename l as x -> x |