From 7c047370dc9032e3ded3365a45de5b92e7c9033f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 14 Oct 2016 22:12:53 +0200
Subject: Fix bug #5139: Anomalies should not be caught by || / try.

There was a catch-all clause in the tclORELSE0 function. We now only
catch noncritical exceptions.
---
 tactics/tacticals.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/tacticals.ml')

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 87fdcf14d..66da9ee18 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -322,7 +322,7 @@ module New = struct
     try
       Refiner.catch_failerror e;
       tclUNIT ()
-    with e -> tclZERO e
+    with e when CErrors.noncritical e -> tclZERO e
 
   (* spiwack: I chose to give the Ltac + the same semantics as
      [Proofview.tclOR], however, for consistency with the or-else
-- 
cgit v1.2.3