From 15effb7dedbaa407bbe25055da6efded366dd3b1 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:35:31 +0000
Subject: Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).

They were a hack to avoid looking where exceptions were raised and not
caught. Hopefully I produce a cleaner stack now, catching errors when
it is needed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16980 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proofview.ml  | 18 +++++-------------
 proofs/proofview.mli |  4 ++++
 2 files changed, 9 insertions(+), 13 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a3791e7a42..eed792fd7f 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -421,22 +421,12 @@ module Notations = struct
   let (>-) = Goal.bind
   let (>=) = tclBIND
   let (>>=) t k =
-    (* spiwack: the application of List.map may raise errors, as this
-       combinator is mostly used in porting historical tactic code,
-       where the error flow is somewhat hard to follow, hence the
-       try/with *)
-      t >= fun l ->
-      try tclDISPATCH (List.map k l)
-      with e when Errors.noncritical e -> tclZERO e
+    t >= fun l ->
+    tclDISPATCH (List.map k l)
   let (>>==) t k =
-    (* spiwack: the application of List.map may raise errors, as this
-       combinator is mostly used in porting historical tactic code,
-       where the error flow is somewhat hard to follow, hence the
-       try/with *)
     begin
       t >= fun l ->
-      try tclDISPATCHL (List.map k l)
-      with e when Errors.noncritical e -> tclZERO e
+      tclDISPATCHL (List.map k l)
     end >= fun l' ->
     tclUNIT (List.flatten l')
   let (<*>) = tclTHEN
@@ -531,6 +521,8 @@ module V82 = struct
 
   let put_status b _env =
     Proof.lift (Message.put b)
+
+  let catchable_exception = Errors.noncritical
 end
 
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 4536180e2e..a2a5746933 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -268,6 +268,10 @@ module V82 : sig
 
   (* marks as unsafe if the argument is [false] *)
   val put_status : bool -> unit tactic
+
+  (* exception for which it is deemed to be safe to transmute into
+     tactic failure. *)
+  val catchable_exception : exn -> bool
 end
 
 
-- 
cgit v1.2.3