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 +---
 proofs/refiner.ml            | 10 +++-------
 tactics/class_tactics.ml     | 11 ++++-------
 tactics/equality.ml          |  3 +--
 4 files changed, 9 insertions(+), 19 deletions(-)

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
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 =
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e3f2f18b44..f92d0603ca 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -234,9 +234,8 @@ let unify_resolve_refine poly flags gl clenv =
       match fst ie with
       | Evarconv.UnableToUnify _ ->
          Tacticals.New.tclZEROMSG (str "Unable to unify")
-      | e when CErrors.noncritical e ->
-         Tacticals.New.tclZEROMSG (str "Unexpected error")
-      | _ -> Exninfo.iraise ie)
+      | e ->
+         Tacticals.New.tclZEROMSG (str "Unexpected error"))
 
 (** Dealing with goals of the form A -> B and hints of the form
   C -> A -> B.
@@ -447,7 +446,7 @@ let cut_of_hints h =
 
 let catchable = function
   | Refiner.FailError _ -> true
-  | e -> Logic.catchable_exception e
+  | e -> Logic.catchable_exception e [@@ocaml.warning "-3"]
 
 let pr_depth l =
   let rec fmt elts =
@@ -769,9 +768,7 @@ module Search = struct
              (with_shelf tac >>= fun s ->
               let i = !idx in incr idx; result s i None)
              (fun e' ->
-              if CErrors.noncritical (fst e') then
-                (pr_error e'; aux (merge_exceptions e e') tl)
-              else Exninfo.iraise e')
+                (pr_error e'; aux (merge_exceptions e e') tl))
     and aux e = function
       | x :: xs -> onetac e x xs
       | [] ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9804d4754d..fb39a856e9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1627,10 +1627,9 @@ let try_rewrite tac =
   Proofview.tclORELSE tac begin function (e, info) -> match e with
     | Constr_matching.PatternMatchingFailure ->
         tclZEROMSG (str "Not a primitive equality here.")
-    | e when catchable_exception e ->
+    | e ->
         tclZEROMSG
           (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
-    | e -> Proofview.tclZERO ~info e
   end
 
 let cutSubstClause l2r eqn cls =
-- 
cgit v1.2.3