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 | 8 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
5 files changed, 15 insertions, 0 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 6b06a05346..ddabb5d089 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -687,6 +687,8 @@ and intern_tactic_seq onlytac ist = function | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac) | TacTimeout (n,tac) -> 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) | 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 0e54ed84cd..abc1daa5b8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1137,6 +1137,8 @@ and eval_tactic ist = function | TacTimeout (n,tac) -> Tacticals.New.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac) | TacTry tac -> Tacticals.New.tclTRY (interp_tactic ist tac) | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac) + | TacOr (tac1,tac2) -> + Tacticals.New.tclOR (interp_tactic ist tac1) (interp_tactic ist tac2) | 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 deac1d4ff1..ba37c10191 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -247,6 +247,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacTry tac -> TacTry (subst_tactic subst tac) | TacInfo tac -> TacInfo (subst_tactic subst tac) | TacRepeat tac -> TacRepeat (subst_tactic subst tac) + | TacOr (tac1,tac2) -> + TacOr (subst_tactic subst tac1,subst_tactic subst tac2) | 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 8156c898ec..74c31fa382 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -383,6 +383,14 @@ module New = struct Refiner.catch_failerror e; tclUNIT () with e -> tclZERO e + + (* spiwack: I chose to give the Ltac + the same semantics as + [Proofview.tclOR], however, for consistency with the or-else + tactical, we may consider wrapping the first argument with + [tclPROGRESS]. It strikes me as a bad idea, but consistency can be + considered valuable. *) + let tclOR = Proofview.Notations.(<+>) + let tclORELSE0 t1 t2 = tclINDEPENDENT begin tclORELSE diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index d0dae09932..f7ba178a31 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -183,6 +183,7 @@ module New : sig (meaning that it will jump over [n] error catching tacticals FROM THIS MODULE. *) val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic + val tclOR : unit tactic -> unit tactic -> unit tactic val tclORELSE0 : unit tactic -> unit tactic -> unit tactic val tclORELSE : unit tactic -> unit tactic -> unit tactic |