From a9cfc4691726ac248dc7bbc43bb5ae8a7db3233f Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:38:38 +0000
Subject: Corrects the semantics of the "+" tactical.

- Treats goals independently
- Honors failure levels

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17003 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacticals.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 224762e0a7..574e4c9a92 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -389,7 +389,14 @@ module New = struct
      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 tclOR t1 t2 =
+    tclINDEPENDENT begin
+      Proofview.tclOR
+        t1
+        begin fun e ->
+          catch_failerror e <*> t2
+        end
+    end
 
   let tclORELSE0 t1 t2 =
     tclINDEPENDENT begin
-- 
cgit v1.2.3