From 3c964a60d698134c21adc77cbb69ce1528350682 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 9 Sep 2017 14:54:42 +0200
Subject: Document UState.universe_context.

---
 engine/uState.mli | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/uState.mli b/engine/uState.mli
index 21145e7e67..c44f2c1d74 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -118,8 +118,17 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 
 val normalize : t -> t
 
-(** {5 TODO: Document me} *)
+(** [universe_context names extensible ctx]
+
+    Return a universe context containing the local universes of [ctx]
+    and their constraints. The universes corresponding to [names] come
+    first in the order defined by that list.
+
+    If [extensible] is false, check that the universes of [names] are
+    the only local universes.
 
+    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.universe_context
 
@@ -128,6 +137,8 @@ type universe_decl =
 
 val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context
 
+(** {5 TODO: Document me} *)
+
 val update_sigma_env : t -> Environ.env -> t
 
 (** {5 Pretty-printing} *)
-- 
cgit v1.2.3