From d66eefb692b0eb825de83782fad95bdcc0e44781 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:41:51 +0000
Subject: A try/with was catching every exception.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17034 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proofview.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 9f87b26ae4..bc251d33de 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -290,7 +290,7 @@ let tclFOCUS i j t =
     Proof.get >>= fun next ->
     Proof.set (unfocus context next) >>
     Proof.ret result
-  with e ->
+  with e when Errors.noncritical e ->
     (* spiwack: a priori the only possible exceptions are that of focus,
        of course I haven't made them algebraic yet. *)
     tclZERO e
-- 
cgit v1.2.3