From 485a0a6280abbef62f7e2c2bfbaf3b73d67bbdaf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Sep 2017 15:23:15 +0200
Subject: Use type Universes.universe_binders.

---
 engine/uState.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/uState.mli')

diff --git a/engine/uState.mli b/engine/uState.mli
index 1c906fcb2d..f54bcc832a 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -135,7 +135,7 @@ val normalize : t -> t
     Also return the association list of universe names and universes
     (including those not in [names]). *)
 val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t ->
-  (Id.t * Univ.Level.t) list * Univ.UContext.t
+  Universes.universe_binders * Univ.UContext.t
 
 type universe_decl =
   (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
-- 
cgit v1.2.3