From ec15eb5d0d0fa4085cc2413d9f6fe5db07feb216 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 24 Jun 2020 15:52:41 +0200
Subject: Remove the catchable-exception related functions.

They were deprecated in 8.12.
---
 tactics/class_tactics.ml  | 4 ----
 tactics/class_tactics.mli | 3 ---
 2 files changed, 7 deletions(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3