diff options
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
| -rw-r--r-- | pretyping/typeclasses_errors.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 980f327cb..1648f667a 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -19,13 +19,14 @@ open Nametab open Mod_subst open Topconstr open Util +open Libnames (*i*) type contexts = Parameters | Properties type typeclass_error = - | UnboundClass of identifier located - | UnboundMethod of identifier * identifier located (* Class name, method *) + | NotAClass of constr + | UnboundMethod of global_reference * identifier located (* Class name, method *) | NoInstance of identifier located * constr list | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *) @@ -33,7 +34,7 @@ exception TypeClassError of env * typeclass_error let typeclass_error env err = raise (TypeClassError (env, err)) -let unbound_class env id = typeclass_error env (UnboundClass id) +let not_a_class env c = typeclass_error env (NotAClass c) let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id)) |