Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
Merge PR #12580: Remove the catchable-exception related functions.
Reviewed-by: ejgallego
  • Loading branch information
ejgallego committed Jun 25, 2020
2 parents ba355fb + ec15eb5 commit 88e7e1d
Show file tree
Hide file tree
Showing 4 changed files with 0 additions and 39 deletions.
29 changes: 0 additions & 29 deletions proofs/logic.ml
Expand Up @@ -20,7 +20,6 @@ open Environ
open Reductionops
open Inductiveops
open Typing
open Type_errors
open Retyping

module NamedDecl = Context.Named.Declaration
Expand All @@ -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))

Expand Down
3 changes: 0 additions & 3 deletions proofs/logic.mli
Expand Up @@ -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 =
Expand Down
4 changes: 0 additions & 4 deletions tactics/class_tactics.ml
Expand Up @@ -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
Expand Down
3 changes: 0 additions & 3 deletions tactics/class_tactics.mli
Expand Up @@ -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
Expand Down

0 comments on commit 88e7e1d

Please sign in to comment.