Merge PR #12580: Remove the catchable-exception related functions.

Reviewed-by: ejgallego

4 files changed, 0 insertions, 39 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index c7a1c32e7c..07ea2ea572 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -20,7 +20,6 @@ open Environ
 open Reductionops
 open Inductiveops
 open Typing
-open Type_errors
 open Retyping
 
 module NamedDecl = Context.Named.Declaration
@@ -40,34 +39,6 @@ type refiner_error =
 
 exception RefinerError of Environ.env * Evd.evar_map * refiner_error
 
-open Pretype_errors
-
-(** FIXME: this is quite brittle. Why not accept any PretypeError? *)
-let is_typing_error = function
-| UnexpectedType (_, _) | NotProduct _
-| VarNotFound _ | TypingError _ -> true
-| _ -> false
-
-let is_unification_error = function
-| CannotUnify _ | CannotUnifyLocal _| CannotGeneralize _
-| NoOccurrenceFound _ | CannotUnifyBindingType _
-| ActualTypeNotCoercible _ | UnifOccurCheck _
-| CannotFindWellTypedAbstraction _ | WrongAbstractionType _
-| UnsolvableImplicit _| AbstractionOverMeta _
-| UnsatisfiableConstraints _ -> true
-| _ -> false
-
-let catchable_exception = function
-  | CErrors.UserError _ | TypeError _
-  | Proof.OpenProof _
-  (* abstract will call close_proof inside a tactic *)
-  | RefinerError _ | Indrec.RecursionSchemeError _
-  | Nametab.GlobalizationError _
-  (* reduction errors *)
-  | Tacred.ReductionTacticError _ -> true
-  (* unification and typing errors *)
-  | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e
-  | _ -> false
 
 let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id))
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 9dc75000a1..21757e47dc 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -47,9 +47,6 @@ exception RefinerError of Environ.env * evar_map * refiner_error
 
 val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a
 
-val catchable_exception : exn -> bool
-[@@ocaml.deprecated "This function does not scale in the presence of dynamically added exceptions. Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."]
-
 (** Move destination for hypothesis *)
 
 type 'id move_location =
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 484aab2f00..b3be420e76 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -446,10 +446,6 @@ let e_possible_resolve db_list local_db secvars only_classes env sigma concl =
 let cut_of_hints h =
   List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
 
-let catchable = function
-  | Refiner.FailError _ -> true
-  | e -> Logic.catchable_exception e [@@ocaml.warning "-3"]
-
 let pr_depth l =
   let rec fmt elts =
     match elts with
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index b97b90d777..381f68f14f 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -15,9 +15,6 @@ 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 set_typeclasses_depth : int option -> unit