Changes the semantics of Ltac's non-lazy pattern matching in presence of multiple successes.

The semantics was a bit strange: an immediate failure of a branch would cause the pattern matching to backtrack, and failure after the match could cause the selected tactic to backtrack. However, the pattern matching process won't backtrack after it has selected a tactic with at least one success.

To avoid changing the semantics of pattern matching with single-success tactics, I made it so that it is impossible to backtrack into a pattern matching once done.

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

1 files changed, 9 insertions, 9 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ffe027474a..6c2ed52877 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1233,18 +1233,18 @@ and interp_match_success ist { TacticMatching.subst ; context ; terms ; lhs } =
     first success is considered, otherwise further successes are tried
     if the left-hand side fails. *)
 and interp_match_successes lz ist s =
-    (** iterates [tclORELSE] lazily on the stream [t], if [t] is
+    (** iterates [tclOR] lazily on the stream [t], if [t] is
         exhausted, raises [e]. Beware: there is no [tclINDEPENDENT],
         relying on the fact that it will always be applied to a single
         goal, by virtue of an earlier [Proofview.Goal.enter]. *)
-    let rec tclORELSE_stream t e =
-      match IStream.peek t with
-      | Some (t1,t') ->
-          Proofview.tclORELSE
-            t1
-            begin fun e ->
+  let rec tclOR_stream t e =
+    match IStream.peek t with
+    | Some (t1,t') ->
+        Proofview.tclORELSE
+          t1
+          begin fun e ->
               (* Honors Ltac's failure level. *)
-              Tacticals.New.catch_failerror e <*> tclORELSE_stream t' e
+              Tacticals.New.catch_failerror e <*> tclOR_stream t' e
             end
       | None ->
           Proofview.tclZERO e
@@ -1263,7 +1263,7 @@ and interp_match_successes lz ist s =
       end
     else
       (** match *)
-      tclORELSE_stream successes matching_failure
+      Proofview.tclONCE (tclOR_stream successes matching_failure)
 
 
 (* Interprets the Match expressions *)