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

1 files changed, 8 insertions, 1 deletions

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