Added the tactical "tac1 + tac2".

It works pretty much like "tac1 || tac2" except that it has as successes all the successes of tac1 followed by all the successes of tac2 (whereas the latter has either the successes of tac1 (if there is at least one) or those of tac2 (otherwise)).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16998 85f007b7-540e-0410-9357-904b9bb8a0f7

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