diff options
| author | Arnaud Spiwack | 2014-07-31 16:08:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-01 19:18:58 +0200 |
| commit | 2925c97c852efd66656edebedba543c7c8335b73 (patch) | |
| tree | befa69018bc1e698b5cc73b616cf44c704ecd9d9 /tactics | |
| parent | a7a3f6510643b4fa4bc3299c5111c44b4887873d (diff) | |
New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.
Differs from the usual t;[t1…tn] in two ways:
* It can be used without a preceding tactic
* It counts every focused subgoal, rather than considering independently the goals generated by the application of the preceding tactic on individual goals.
In other words t;[t1…tn] is [> t;[>t1…tn].. ].
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 7 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 6 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 5 |
3 files changed, 18 insertions, 0 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 324ea2f049..2a66b32bc5 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -593,6 +593,13 @@ and intern_tactic_seq onlytac ist = function let lfun', t1 = intern_tactic_seq onlytac ist t1 in let lfun'', t2 = intern_tactic_seq onlytac { ist with ltacvars = lfun' } t2 in lfun'', TacThen (t1,t2) + | TacDispatch tl -> + ist.ltacvars , TacDispatch (List.map (intern_pure_tactic ist) tl) + | TacExtendTac (tf,t,tl) -> + ist.ltacvars , + TacExtendTac (Array.map (intern_pure_tactic ist) tf, + intern_pure_tactic ist t, + Array.map (intern_pure_tactic ist) tl) | TacThens3parts (t1,tf,t2,tl) -> let lfun', t1 = intern_tactic_seq onlytac ist t1 in let ist' = { ist with ltacvars = lfun' } in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1eecb94972..20234d1f2c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1042,6 +1042,12 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with end | TacThen (t1,t) -> Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t) + | TacDispatch tl -> + Proofview.tclDISPATCH (List.map (interp_tactic ist) tl) + | TacExtendTac (tf,t,tl) -> + Proofview.tclEXTEND (Array.map_to_list (interp_tactic ist) tf) + (interp_tactic ist t) + (Array.map_to_list (interp_tactic ist) tl) | TacThens (t1,tl) -> Tacticals.New.tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl) | TacThens3parts (t1,tf,t,tl) -> Tacticals.New.tclTHENS3PARTS (interp_tactic ist t1) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index ecadfca593..30fffed911 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -225,6 +225,11 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s) | TacThen (t1,t2) -> TacThen (subst_tactic subst t1, subst_tactic subst t2) + | TacDispatch tl -> TacDispatch (List.map (subst_tactic subst) tl) + | TacExtendTac (tf,t,tl) -> + TacExtendTac (Array.map (subst_tactic subst) tf, + subst_tactic subst t, + Array.map (subst_tactic subst) tl) | TacThens (t,tl) -> TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl) | TacThens3parts (t1,tf,t2,tl) -> |