From 89a5abb0b8b453bdda8c9ebf33734c42c3a826db Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 2 Mar 2020 21:15:04 +0100
Subject: Removing catchable_exception test in tclOR/tclORELSE.

Since tclOR/tclORELSE are not supposed to return critical exceptions,
we don't need to replace catchable_exception by noncritical.
---
 proofs/refiner.ml | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index fd73ab1b5a..825cd938fb 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -204,14 +204,10 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
 
 
 let catch_failerror (e, info) =
-  if catchable_exception e then Control.check_for_interrupt ()
-  else match e with
-  | FailError (0,_) ->
-      Control.check_for_interrupt ()
-  | FailError (lvl,s) ->
+  match e with
+  | FailError (lvl,s) when lvl > 0 ->
     Exninfo.iraise (FailError (lvl - 1, s), info)
-  | e -> Exninfo.iraise (e, info)
-  (** FIXME: do we need to add a [Errors.push] here? *)
+  | e -> Control.check_for_interrupt ()
 
 (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
 let tclORELSE0 t1 t2 g =
-- 
cgit v1.2.3