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

9 files changed, 28 insertions, 1 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index b1150d6c04..d0fd618c7f 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -453,6 +453,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
       <:expr< Tacexpr.TacSolve $mlexpr_of_list mlexpr_of_tactic tl$ >>
   | Tacexpr.TacTry t ->
       <:expr< Tacexpr.TacTry $mlexpr_of_tactic t$ >>
+  | Tacexpr.TacOr (t1,t2) ->
+      <:expr< Tacexpr.TacOr $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >>
   | Tacexpr.TacOrelse (t1,t2) ->
       <:expr< Tacexpr.TacOrelse $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >>
   | Tacexpr.TacDo (n,t) ->
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index df4ed2c41e..fece993120 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -214,6 +214,9 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
   | TacComplete of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacSolve of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr list
   | TacTry of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
+  | TacOr of
+      ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr *
+      ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacOrelse of
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr *
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index e0a1c046a4..96f4bc387f 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -73,7 +73,9 @@ GEXTEND Gram
           TacAbstract (tc,Some s) ]
 (*End of To do*)
     | "2" RIGHTA
-      [ ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1)
+      [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1)
+      | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) 
+      | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1)
       | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
     | "1" RIGHTA
       [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index a771184716..61f758df01 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -886,6 +886,11 @@ let rec pr_tac inherited tac =
   | TacInfo t ->
       hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t),
       linfo
+  | TacOr (t1,t2) ->
+      (* arnaud: vérifier qu'il s'agit bien de la syntaxe définitive. *)
+      hov 1 (pr_tac (lorelse,L) t1 ++ str " +" ++ brk (1,1) ++
+             pr_tac (lorelse,E) t2),
+      lorelse
   | TacOrelse (t1,t2) ->
       hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
              pr_tac (lorelse,E) t2),
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