Merge PR #11735: Deprecating catchable_exception

Reviewed-by: ejgallego
Reviewed-by: ppedrot

4 files changed, 13 insertions, 18 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 69ab23aa55..321b05b97c 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -129,7 +129,7 @@ let find_class_proof proof_type proof_method env evars carrier relation =
     let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) goal in
       if extends_undefined (goalevars evars) evars' then raise Not_found
       else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |]
-  with e when Logic.catchable_exception e -> raise Not_found
+  with e when CErrors.noncritical e -> raise Not_found
 
 (** Utility functions *)
 
@@ -724,8 +724,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs)
     let rew = if l2r then rew else symmetry env sort rew in
     Some rew
   with
-  | e when Class_tactics.catchable e -> None
-  | Reduction.NotConvertible -> None
+  | e when noncritical e -> None
 
 let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t =
   try
@@ -741,8 +740,7 @@ let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t =
     let rew = if l2r then rew else symmetry env sort rew in
     Some rew
   with
-  | e when Class_tactics.catchable e -> None
-  | Reduction.NotConvertible -> None
+  | e when noncritical e -> None
 
 type rewrite_flags = { under_lambdas : bool; on_morphisms : bool }
 
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 762f858b82..597c3fdaac 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -363,7 +363,7 @@ let intern_typed_pattern ist ~as_type ~ltacvars p =
 let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
   let interp_ref r =
     try Inl (intern_evaluable ist r)
-    with e when Logic.catchable_exception e ->
+    with e when CErrors.noncritical e ->
       (* Compatibility. In practice, this means that the code above
          is useless. Still the idea of having either an evaluable
          ref or a pattern seems interesting, with "head" reduction
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index eeefeeb4f8..5fbea4eeef 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/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 4cec2c5a52..2eef459217 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -25,7 +25,6 @@ open EConstr
 open Tacticals.New
 open Tacmach.New
 open Tactics
-open Logic
 open Libnames
 open Nametab
 open Contradiction
@@ -971,7 +970,7 @@ let rec transform sigma p t =
        tac @ tac', t''
    | Kapp(Z_of_nat,[t']) -> default true t'
    | _ -> default false t
-  with e when catchable_exception e -> default false t
+  with e when noncritical e -> default false t
 
 let shrink_pair p f1 f2 =
   match f1,f2 with
@@ -1420,7 +1419,7 @@ let destructure_omega env sigma tac_def (id,c) =
           normalize_equation sigma
             id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def
       | _ -> tac_def
-    with e when catchable_exception e -> tac_def
+    with e when noncritical e -> tac_def
 
 let reintroduce id =
   (* [id] cannot be cleared if dependent: protect it by a try *)
@@ -1527,7 +1526,7 @@ let nat_inject =
                 Kapp(S,[t]) -> is_number t
               | Kapp(O,[]) -> true
               | _ -> false
-            with e when catchable_exception e -> false
+            with e when noncritical e -> false
           in
           let rec loop p t : unit Proofview.tactic =
             try match destructurate_term sigma t with
@@ -1538,7 +1537,7 @@ let nat_inject =
                         ((Lazy.force coq_inj_S),[t]))
                      (loop (P_APP 1 :: p) t))
               | _ -> explore p t
-            with e when catchable_exception e -> explore p t
+            with e when noncritical e -> explore p t
           in
           if is_number t' then focused_simpl p else loop p t
       | Kapp(Pred,[t]) ->
@@ -1551,7 +1550,7 @@ let nat_inject =
             (explore p t_minus_one)
       | Kapp(O,[]) -> focused_simpl p
       | _ -> Proofview.tclUNIT ()
-    with e when catchable_exception e -> Proofview.tclUNIT ()
+    with e when noncritical e -> Proofview.tclUNIT ()
 
   and loop = function
     | [] -> Proofview.tclUNIT ()
@@ -1615,7 +1614,7 @@ let nat_inject =
                   ]
                 else loop lit
             | _ -> loop lit
-          with e when catchable_exception e -> loop lit end
+          with e when noncritical e -> loop lit end
   in
   let hyps_types = Tacmach.New.pf_hyps_types gl in
   loop (List.rev hyps_types)
@@ -1725,7 +1724,7 @@ let destructure_hyps =
                 (assert_by (Name hid) hty reflexivity)
                 (loop (LocalAssum (make_annot hid Sorts.Relevant, hty) :: lit))
            | _ -> loop lit
-         with e when catchable_exception e -> loop lit
+         with e when noncritical e -> loop lit
        end
     | decl :: lit -> (* variable without body (or !letin_flag isn't set) *)
        let i = NamedDecl.get_id decl in
@@ -1857,7 +1856,7 @@ let destructure_hyps =
           | _ -> loop lit
             with
             | Undecidable -> loop lit
-            | e when catchable_exception e -> loop lit
+            | e when noncritical e -> loop lit
           end
     in
     let hyps = Proofview.Goal.hyps gl in