Move UnsatisfiableConstraints to a pretype error.

5 files changed, 31 insertions, 31 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 934e7bdbb..cad0beabf 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -51,6 +51,8 @@ type pretype_error =
   | NotProduct of constr
   | TypingError of type_error
   | CannotUnifyOccurrences of subterm_unification_error
+  | UnsatisfiableConstraints of
+    (existential_key * Evar_kinds.t) option * Evar.Set.t option
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
@@ -150,3 +152,20 @@ let error_not_product_loc loc env sigma c =
 
 let error_var_not_found_loc loc s =
   raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s)
+
+(*s Typeclass errors *)
+
+let unsatisfiable_constraints env evd ev comp =
+  match ev with
+  | None ->
+    let err = UnsatisfiableConstraints (None, comp) in
+    raise (PretypeError (env,evd,err))
+  | Some ev ->
+    let loc, kind = Evd.evar_source ev evd in
+    let err = UnsatisfiableConstraints (Some (ev, kind), comp) in
+    Loc.raise loc (PretypeError (env,evd,err))
+
+let unsatisfiable_exception exn =
+  match exn with
+  | PretypeError (_, _, UnsatisfiableConstraints _) -> true
+  | _ -> false
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index e816463e7..cc1443162 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -52,6 +52,9 @@ type pretype_error =
   | NotProduct of constr
   | TypingError of type_error
   | CannotUnifyOccurrences of subterm_unification_error
+  | UnsatisfiableConstraints of
+    (existential_key * Evar_kinds.t) option * Evar.Set.t option
+    (** unresolvable evar, connex component *)
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
@@ -134,3 +137,11 @@ val error_not_product_loc :
 (** {6 Error in conversion from AST to glob_constr } *)
 
 val error_var_not_found_loc : Loc.t -> Id.t -> 'b
+
+(** {6 Typeclass errors } *)
+
+val unsatisfiable_constraints : env -> Evd.evar_map -> Evd.evar option ->
+  Evar.Set.t option -> 'a
+
+val unsatisfiable_exception : exn -> bool
+
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
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index b3cfb37fa..c2a295bbc 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -20,10 +20,6 @@ type contexts = Parameters | Properties
 type typeclass_error =
   | NotAClass of constr
   | UnboundMethod of global_reference * Id.t located (** Class name, method *)
-  | NoInstance of Id.t located * constr list
-  | UnsatisfiableConstraints of
-    evar_map * (existential_key * Evar_kinds.t) option * Evar.Set.t option
-    (** evar map, unresolvable evar, connex component *)
   | MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *)
 
 exception TypeClassError of env * typeclass_error
@@ -32,11 +28,5 @@ val not_a_class : env -> constr -> 'a
 
 val unbound_method : env -> global_reference -> Id.t located -> 'a
 
-val no_instance : env -> Id.t located -> constr list -> 'a
-
-val unsatisfiable_constraints : env -> evar_map -> evar option ->
-  Evar.Set.t option -> 'a
-
 val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a
 
-val unsatisfiable_exception : exn -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ed01c6b7b..5f7e2916b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1337,7 +1337,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
        if closed0 cl && not (isEvar cl)
        then
 	 (try w_typed_unify env evd CONV flags op cl,cl
-	  with ex when Typeclasses_errors.unsatisfiable_exception ex ->
+	  with ex when Pretype_errors.unsatisfiable_exception ex ->
 	    bestexn := Some ex; error "Unsat")
        else error "Bound 1"
      with ex when precatchable_exception ex ->