diff options
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
| -rw-r--r-- | pretyping/typeclasses_errors.mli | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index fbc2f25449..82e37f41d8 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -19,21 +19,22 @@ 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 *) exception TypeClassError of env * typeclass_error -val unbound_class : env -> identifier located -> 'a +val not_a_class : env -> constr -> 'a -val unbound_method : env -> identifier -> identifier located -> 'a +val unbound_method : env -> global_reference -> identifier located -> 'a val no_instance : env -> identifier located -> constr list -> 'a |