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".

5 files changed, 14 insertions, 12 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 0fb32e5150..498a9d9825 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -832,7 +832,7 @@ let empty = {
   extras = Store.empty;
 }
 
-let from_env e = { empty with universes = UState.from_env e }
+let from_env ?binders e = { empty with universes = UState.from_env ?binders e }
 
 let from_ctx uctx = { empty with universes = uctx }
 
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 *)
diff --git a/engine/uState.ml b/engine/uState.ml
index d5be6e1b37..103b552d86 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -63,8 +63,6 @@ let make ~lbound univs =
     universes_lbound = lbound;
     initial_universes = univs}
 
-let from_env env = make ~lbound:(Environ.universes_lbound env) (Environ.universes env)
-
 let is_empty uctx =
   ContextSet.is_empty uctx.local &&
     LMap.is_empty uctx.univ_variables
@@ -606,13 +604,16 @@ let new_univ_variable ?loc rigid name uctx =
 
 let add_global_univ uctx u = add_universe None true UGraph.Bound.Set uctx u
 
-let make_with_initial_binders ~lbound e us =
-  let uctx = make ~lbound e in
+let make_with_initial_binders ~lbound univs us =
+  let uctx = make ~lbound univs in
   List.fold_left
     (fun uctx { CAst.loc; v = id } ->
        fst (new_univ_variable ?loc univ_rigid (Some id) uctx))
     uctx us
 
+let from_env ?(binders=[]) env =
+  make_with_initial_binders ~lbound:(Environ.universes_lbound env) (Environ.universes env) binders
+
 let make_flexible_variable uctx ~algebraic u =
   let {local = cstrs; univ_variables = uvars;
        univ_algebraic = avars; universes=g; } = uctx in
diff --git a/engine/uState.mli b/engine/uState.mli
index bb26f0f821..d79447f6a9 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -28,12 +28,14 @@ type t
 val empty : t
 
 val make : lbound:UGraph.Bound.t -> UGraph.t -> t
+[@@ocaml.deprecated "Use from_env"]
 
 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 : Environ.env -> t
+val from_env : ?binders:lident list -> Environ.env -> t
 
 val of_context_set : Univ.ContextSet.t -> t
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e09ee150d5..cdec8b8817 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2586,11 +2586,10 @@ let interp_univ_constraints env evd cstrs =
 
 let interp_univ_decl env decl =
   let open UState in
-  let pl : lident list = decl.univdecl_instance in
-  let evd = Evd.from_ctx (UState.make_with_initial_binders ~lbound:(Environ.universes_lbound env)
-                            (Environ.universes env) pl) in
+  let binders : lident list = decl.univdecl_instance in
+  let evd = Evd.from_env ~binders env in
   let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
-  let decl = { univdecl_instance = pl;
+  let decl = { univdecl_instance = binders;
     univdecl_extensible_instance = decl.univdecl_extensible_instance;
     univdecl_constraints = cstrs;
     univdecl_extensible_constraints = decl.univdecl_extensible_constraints }