aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses_errors.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
-rw-r--r--pretyping/typeclasses_errors.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index fd709763d1..3feb652ae3 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -25,7 +25,7 @@ type typeclass_error =
| NotAClass of constr
| UnboundMethod of global_reference * identifier located (** Class name, method *)
| NoInstance of identifier located * constr list
- | UnsatisfiableConstraints of evar_map * (existential_key * hole_kind) option
+ | UnsatisfiableConstraints of evar_map * (existential_key * Evar_kinds.t) option
| MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *)
exception TypeClassError of env * typeclass_error