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.

---
 toplevel/classes.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'toplevel/classes.mli')

diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 24c51b31a3..d600b3104f 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -31,8 +31,9 @@ val declare_instance_constant :
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Globnames.global_reference -> unit) ->
   Id.t -> (** name *)
+  Id.t Loc.located list option ->
   bool -> (* polymorphic *)
-  Univ.universe_context_set -> (* Universes *)
+  Evd.evar_map -> (* Universes *)
   Constr.t -> (** body *)
   Term.types -> (** type *)
   Names.Id.t
-- 
cgit v1.2.3