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.
---
 proofs/logic.ml  | 29 -----------------------------
 proofs/logic.mli |  3 ---
 2 files changed, 32 deletions(-)

(limited to 'proofs')

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