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 ----
 1 file changed, 4 deletions(-)

(limited to 'tactics/class_tactics.ml')

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