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.
---
 plugins/ltac/tactic_debug.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 3512bb936d..cef0f62a90 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -229,9 +229,7 @@ let debug_prompt lev tac f =
       Proofview.tclTHEN
         (Proofview.tclLIFT begin
           (skip:=0) >> (skipped:=0) >>
-            if Logic.catchable_exception reraise then
-              msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ explain_logic_error reraise)
-            else return ()
+          msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ explain_logic_error reraise)
         end)
         (Proofview.tclZERO ~info reraise)
     end
-- 
cgit v1.2.3