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

3 files changed, 9 insertions, 12 deletions

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