From 4814c482eb83f4c21b6ecf2b1b9235b513221181 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Oct 2020 14:34:17 +0100
Subject: Factorizing UState.make* through UState.from_env, to highlight the
 similarity.

An alternative could also be to split the initialization of the
environment and the declaration of initial "binders".
---
 engine/evd.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index fafaad9a04..40957774fe 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -153,9 +153,9 @@ type evar_map
 val empty : evar_map
 (** The empty evar map. *)
 
-val from_env : env -> 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. *)
+    universes from env, possibly with initial universe binders. *)
 
 val from_ctx : UState.t -> evar_map
 (** The empty evar map with given universe context *)
-- 
cgit v1.2.3


From e7b39c73f48279980f8ea2238632bfbf6e3d4178 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Oct 2020 14:56:19 +0100
Subject: Documentation of the main entry points of uState.mli.

---
 engine/evd.mli | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'engine/evd.mli')

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. *)
-- 
cgit v1.2.3