diff options
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 324ea2f04..2a66b32bc 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 1eecb9497..20234d1f2 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 ecadfca59..30fffed91 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) -> |