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

7 files changed, 14 insertions, 18 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
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5323c9f1c6..bb640a83f6 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -385,7 +385,7 @@ let build_beq_scheme mode kn =
           Vars.substl subst cores.(i)
         in
         create_input fix),
-       UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()))
+       UState.from_env (Global.env ()))
 
 let beq_scheme_kind =
   declare_mutual_scheme_object "_beq"
@@ -707,7 +707,7 @@ let make_bl_scheme mode mind =
   let lnonparrec,lnamesparrec = (* TODO subst *)
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let bl_goal = compute_bl_goal ind lnamesparrec nparrec in
-  let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+  let uctx = UState.from_env (Global.env ()) in
   let side_eff = side_effect_of_mode mode in
   let bl_goal = EConstr.of_constr bl_goal in
   let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
@@ -840,7 +840,7 @@ let make_lb_scheme mode mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal = compute_lb_goal ind lnamesparrec nparrec in
-  let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+  let uctx = UState.from_env (Global.env ()) in
   let side_eff = side_effect_of_mode mode in
   let lb_goal = EConstr.of_constr lb_goal in
   let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
@@ -1010,7 +1010,7 @@ let make_eq_decidability mode mind =
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
   let u = Univ.Instance.empty in
-  let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
+  let uctx = UState.from_env (Global.env ()) in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let side_eff = side_effect_of_mode mode in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index c291890dce..76f79eb0d6 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1641,7 +1641,7 @@ let obligation_terminator entries uctx {name; num; auto} =
            universes and constraints if any *)
         defined
       then
-        UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
+        UState.from_env (Global.env ())
       else uctx
     in
     update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto
@@ -1673,9 +1673,7 @@ let obligation_admitted_terminator {name; num; auto} ctx' dref =
     if not prg.prg_poly (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
-      let ctx =
-        UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
-      in
+      let ctx = UState.from_env (Global.env ()) in
       let ctx' = UState.merge_subst ctx (UState.subst ctx') in
       (Univ.Instance.empty, ctx')
     else
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5fdee9f2d4..bbc20d5e30 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -191,10 +191,9 @@ and solve_obligation_by_tac prg obls i tac =
           obls.(i) <- obl';
           if def && not prg.prg_poly then (
             (* Declare the term constraints with the first obligation only *)
-            let evd = Evd.from_env (Global.env ()) in
-            let evd = Evd.merge_universe_subst evd (UState.subst ctx) in
-            let ctx' = Evd.evar_universe_context evd in
-            Some (ProgramDecl.set_uctx ~uctx:ctx' prg))
+            let uctx = UState.from_env (Global.env ()) in
+            let uctx = UState.merge_subst uctx (UState.subst ctx) in
+            Some (ProgramDecl.set_uctx ~uctx prg))
           else Some prg
       else None