From 5cbcc8fd761df0779f6202fef935f07cfef8a228 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 23 Jan 2016 15:17:29 -0500
Subject: Implement support for universe binder lists in Instance and Program
 Fixpoint/Definition.

---
 intf/constrexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

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
 
-- 
cgit v1.2.3