Move UnsatisfiableConstraints to a pretype error.

1 files changed, 0 insertions, 20 deletions

diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index b16f000d4..816f03321 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -21,9 +21,6 @@ type contexts = Parameters | Properties
 type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of global_reference * Id.t Loc.located (* Class name, method *)
-    | NoInstance of Id.t Loc.located * constr list
-    | UnsatisfiableConstraints of
-      evar_map * (existential_key * Evar_kinds.t) option * Evar.Set.t option
     | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
@@ -34,21 +31,4 @@ let not_a_class env c = typeclass_error env (NotAClass c)
 
 let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
 
-let no_instance env id args = typeclass_error env (NoInstance (id, args))
-
-let unsatisfiable_constraints env evd ev comp =
-  match ev with
-  | None ->
-    let err = UnsatisfiableConstraints (evd, None, comp) in
-    raise (TypeClassError (env, err))
-  | Some ev ->
-    let loc, kind = Evd.evar_source ev evd in
-    let err = UnsatisfiableConstraints (evd, Some (ev, kind), comp) in
-    Loc.raise loc (TypeClassError (env, err))
-
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
-
-let unsatisfiable_exception exn =
-  match exn with
-  | TypeClassError (_, UnsatisfiableConstraints _) -> true
-  | _ -> false