From a5feb9687819c5e7ef0db6e7b74d0e236a296674 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Sep 2017 21:01:57 +0200
Subject: Separate checking univ_decls and obtaining universe binder names.

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

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 63c6752211..889050d90a 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2882,7 +2882,8 @@ 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 ->
-                           Universes.universe_binders * Univ.UContext.t
+      Univ.UContext.t
+    val universe_binders : evar_map -> Universes.universe_binders
     val nf_constraints : evar_map -> evar_map
     val from_ctx : UState.t -> evar_map
 
-- 
cgit v1.2.3