aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/constrexpr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index dcdbd47f68..a53238dfd8 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -121,7 +121,7 @@ and constr_notation_substitution =
constr_expr list list * (** for recursive notations *)
local_binder list list (** for binders subexpressions *)
-type typeclass_constraint = Name.t located * binding_kind * constr_expr
+type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list