Merge PR #11735: Deprecating catchable_exception

Reviewed-by: ejgallego
Reviewed-by: ppedrot

5 files changed, 15 insertions, 18 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index d9009da455..92d56d2904 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -189,7 +189,7 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
   Proofview.Goal.enter begin fun gls ->
     let resolve =
       try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls)
-      with e -> Proofview.tclZERO e
+      with e when noncritical e -> Proofview.tclZERO e
     in resolve >>= fun clenv' ->
        Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
   end
@@ -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.
@@ -459,7 +458,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 =
@@ -785,9 +784,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/class_tactics.mli b/tactics/class_tactics.mli
index c484191a6f..e26338436d 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -16,6 +16,7 @@ open EConstr
 val typeclasses_db : string
 
 val catchable : exn -> bool
+[@@ocaml.deprecated "Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."]
 
 val set_typeclasses_debug : bool -> unit
 val get_typeclasses_debug : unit -> bool
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6e859d997b..49645d82a4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -563,7 +563,7 @@ let apply_special_clear_request clear_flag f =
       let (sigma, (c, bl)) = f env sigma in
       apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
     with
-      e when catchable_exception e -> tclIDTAC
+      e when noncritical e -> tclIDTAC
   end
 
 type multi =
@@ -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 =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index ffa54bab93..a907b9e783 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -926,7 +926,7 @@ let make_resolve_hyp env sigma decl =
        (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
     | Failure _ -> []
-    | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp.")
+    | e when noncritical e -> anomaly (Pp.str "make_resolve_hyp.")
 
 (* REM : in most cases hintname = id *)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c5cd98d386..30ca024a2f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -853,7 +853,7 @@ let change_on_subterm ~check cv_pb deep t where env sigma c =
   let sigma = if !mayneedglobalcheck then
     begin
       try fst (Typing.type_of env sigma c)
-      with e when catchable_exception e ->
+      with e when noncritical e ->
         error "Replacement would lead to an ill-typed term."
     end else sigma
   in
@@ -1313,7 +1313,7 @@ let cut c =
     (* Backward compat: ensure that [c] is well-typed. Plus we need to
        know the relevance *)
     match Typing.sort_of env sigma c with
-    | exception e when Pretype_errors.precatchable_exception e ->
+    | exception e when noncritical e ->
       Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
     | sigma, s ->
       let r = Sorts.relevance_of_sort s in
@@ -1717,7 +1717,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
         if n<0 then error "Applied theorem does not have enough premises.";
         let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
         Clenvtac.res_pf clause ~with_evars ~flags
-      with exn when catchable_exception exn ->
+      with exn when noncritical exn ->
         Proofview.tclZERO exn
     in
     let rec try_red_apply thm_ty (exn0, info) =
@@ -1818,7 +1818,7 @@ let apply_list = function
 let find_matching_clause unifier clause =
   let rec find clause =
     try unifier clause
-    with e when catchable_exception e ->
+    with e when noncritical e ->
     try find (clenv_push_prod clause)
     with NotExtensibleClause -> failwith "Cannot apply"
   in find clause
@@ -4486,7 +4486,7 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
         error "Need a fully applied argument.";
       (* We lose the possibility of coercions in with-bindings *)
       pose_all_metas_as_evars env indclause.evd (clenv_value indclause)
-    with e when catchable_exception e ->
+    with e when noncritical e ->
     try find_clause (try_red_product env sigma typ)
     with Redelimination -> raise e in
   find_clause typ
@@ -5041,7 +5041,7 @@ let unify ?(state=TransparentState.full) x y =
     in
     let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in
     Proofview.Unsafe.tclEVARS sigma
-  with e when CErrors.noncritical e ->
+  with e when noncritical e ->
     Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None)))
   end