Documentation of the main entry points of uState.mli.

2 files changed, 15 insertions, 4 deletions

diff --git a/engine/evd.mli b/engine/evd.mli
index 40957774fe..1c5c65924c 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -155,10 +155,16 @@ val empty : evar_map
 
 val from_env : ?binders:lident list -> env -> evar_map
 (** The empty evar map with given universe context, taking its initial
-    universes from env, possibly with initial universe binders. *)
+    universes from env, possibly with initial universe binders. This
+    is the main entry point at the beginning of the process of
+    interpreting a declaration (e.g. before entering the
+    interpretation of a Theorem statement). *)
 
 val from_ctx : UState.t -> evar_map
-(** The empty evar map with given universe context *)
+(** The empty evar map with given universe context. This is the main
+    entry point when resuming from a already interpreted declaration
+    (e.g.  after having interpreted a Theorem statement and preparing
+    to open a goal). *)
 
 val is_empty : evar_map -> bool
 (** Whether an evarmap is empty. *)
diff --git a/engine/uState.mli b/engine/uState.mli
index d79447f6a9..bd3aac0d8b 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -33,11 +33,16 @@ val make : lbound:UGraph.Bound.t -> UGraph.t -> t
 val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
 [@@ocaml.deprecated "Use from_env"]
 
-val of_binders : UnivNames.universe_binders -> t
-
 val from_env : ?binders:lident list -> Environ.env -> t
+(** Main entry point at the beginning of a declaration declaring the
+    binding names as rigid universes. *)
+
+val of_binders : UnivNames.universe_binders -> t
+(** Main entry point when only names matter, e.g. for printing. *)
 
 val of_context_set : Univ.ContextSet.t -> t
+(** Main entry point when starting from the instance of a global
+    reference, e.g. when building a scheme. *)
 
 (** Misc *)