diff options
| author | Matthieu Sozeau | 2016-01-23 15:17:29 -0500 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-01-23 15:58:06 -0500 |
| commit | 5cbcc8fd761df0779f6202fef935f07cfef8a228 (patch) | |
| tree | 886d05ab59b157b812879facc6ef3fa3defc7d20 /intf | |
| parent | ccdc62a6b4722c38f2b37cbf21b14e5094255390 (diff) | |
Implement support for universe binder lists in Instance and Program Fixpoint/Definition.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 2 |
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 |