From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- pretyping/typeclasses_errors.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'pretyping/typeclasses_errors.ml') 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)) -- cgit v1.2.3