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.

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

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 1f1b05eadb..d912dc7714 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2882,7 +2882,7 @@ sig
     val evar_ident : evar -> evar_map -> Names.Id.t option
     val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
     val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map ->
-                           (Names.Id.t * Univ.Level.t) list * Univ.UContext.t
+                           Universes.universe_binders * Univ.UContext.t
     val nf_constraints : evar_map -> evar_map
     val from_ctx : UState.t -> evar_map
 
-- 
cgit v1.2.3