[universes] [api] Provide UState.from_env

This seems like a recurring pattern, and IMO makes a bit better API.

We also remove `merge_universe_subst` as it is not needed so far, as
we were creating stale `evar_map`s just for this purpose.

4 files changed, 5 insertions, 6 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 5642145f6d..ff13676818 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -697,8 +697,7 @@ let empty = {
   extras = Store.empty;
 }
 
-let from_env e =
-  { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) }
+let from_env e = { empty with universes = UState.from_env e }
 
 let from_ctx ctx = { empty with universes = ctx }
 
@@ -862,9 +861,6 @@ let universe_subst evd =
 let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
   {evd with universes = UState.merge ?loc ~sideff rigid evd.universes ctx'}
 
-let merge_universe_subst evd subst =
-  {evd with universes = UState.merge_subst evd.universes subst }
-
 let with_context_set ?loc rigid d (a, ctx) =
   (merge_context_set ?loc rigid d ctx, a)
 
diff --git a/engine/evd.mli b/engine/evd.mli
index c6c4a71b22..d9b7bd76e7 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -636,7 +636,6 @@ val merge_universe_context : evar_map -> UState.t -> evar_map
 val set_universe_context : evar_map -> UState.t -> evar_map
 
 val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map
-val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map
 
 val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 99ac5f2ce8..7c60d8317c 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -63,6 +63,8 @@ let make ~lbound u =
     uctx_universes_lbound = lbound;
     uctx_initial_universes = u}
 
+let from_env e = make ~lbound:(Environ.universes_lbound e) (Environ.universes e)
+
 let is_empty ctx =
   ContextSet.is_empty ctx.uctx_local &&
     LMap.is_empty ctx.uctx_univ_variables
diff --git a/engine/uState.mli b/engine/uState.mli
index 533a501b59..45a0f9964e 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -29,6 +29,8 @@ val make : lbound:UGraph.Bound.t -> UGraph.t -> t
 
 val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
 
+val from_env : Environ.env -> t
+
 val is_empty : t -> bool
 
 val union : t -> t -> t