diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
5 files changed, 9 insertions, 0 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index ddabb5d08..2f41ff2ae 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -689,6 +689,8 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac) | TacOr (tac1,tac2) -> ist.ltacvars, TacOr (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) + | TacOnce tac -> + ist.ltacvars, TacOnce (intern_pure_tactic ist tac) | TacOrelse (tac1,tac2) -> ist.ltacvars, TacOrelse (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 2bf3c8e06..34ea3dc87 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1139,6 +1139,8 @@ and eval_tactic ist = function | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac) | TacOr (tac1,tac2) -> Tacticals.New.tclOR (interp_tactic ist tac1) (interp_tactic ist tac2) + | TacOnce tac -> + Tacticals.New.tclONCE (interp_tactic ist tac) | TacOrelse (tac1,tac2) -> Tacticals.New.tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2) | TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index ba37c1019..44327abef 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -249,6 +249,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacRepeat tac -> TacRepeat (subst_tactic subst tac) | TacOr (tac1,tac2) -> TacOr (subst_tactic subst tac1,subst_tactic subst tac2) + | TacOnce tac -> + TacOnce (subst_tactic subst tac) | TacOrelse (tac1,tac2) -> TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2) | TacFirst l -> TacFirst (List.map (subst_tactic subst) l) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 574e4c9a9..2131dc480 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -398,6 +398,8 @@ module New = struct end end + let tclONCE = Proofview.tclONCE + let tclORELSE0 t1 t2 = tclINDEPENDENT begin tclORELSE diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index f7ba178a3..722cb8b13 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -184,6 +184,7 @@ module New : sig THIS MODULE. *) val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic val tclOR : unit tactic -> unit tactic -> unit tactic + val tclONCE : unit tactic -> unit tactic val tclORELSE0 : unit tactic -> unit tactic -> unit tactic val tclORELSE : unit tactic -> unit tactic -> unit tactic |