From 7ed370257e576dd084f89eae52fcc2135d4fbee3 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 3 Jul 2014 15:55:00 +0200
Subject: Fix a oversight in 5bf9e67b .

About 8 months after making this commit, I realised that I forgot to change a tclORELSE into a tclOR (which was the whole point of the commit to begin with). Shame on me.

It does not seem to have much of an effect on efficiency, though. It may be a hair faster, but mostly indistinguishably so.
---
 tactics/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c749e2d720..9d8bc68431 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1243,7 +1243,7 @@ and interp_match_successes lz ist s : typed_generic_argument GTac.t =
     match peek t with
     | Nil -> Proofview.tclZERO e
     | Cons (t1,t') ->
-        Proofview.tclORELSE
+        Proofview.tclOR
           (interp_match_success ist t1)
           begin fun e ->
               (* Honors Ltac's failure level. *)
-- 
cgit v1.2.3