diff options
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
| -rw-r--r-- | pretyping/typeclasses_errors.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index e10c81c2..2720a3e4 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -9,18 +9,16 @@ (************************************************************************) (*i*) +open Names open EConstr open Environ -open Constrexpr -open Globnames (*i*) type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr - | UnboundMethod of global_reference * Misctypes.lident (* Class name, method *) - | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *) + | UnboundMethod of GlobRef.t * lident (* Class name, method *) exception TypeClassError of env * typeclass_error @@ -29,5 +27,3 @@ let typeclass_error env err = raise (TypeClassError (env, err)) let not_a_class env c = typeclass_error env (NotAClass c) let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id)) - -let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m)) |