Update update_global_env usage

- take just a ugraph instead of the whole env
- rename to update_sigma_univs
- push global env lookup a bit further up
- fix vernacinterp call to update all surrounding proofs, not just the
  top one
- flip argument order for nicer partial applications

6 files changed, 11 insertions, 10 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 555c3a150c..b20700143f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1160,8 +1160,8 @@ let universe_binders evd = UState.universe_binders evd.universes
 
 let universes evd = UState.ugraph evd.universes
 
-let update_sigma_env evd env =
-  { evd with universes = UState.update_sigma_env evd.universes env }
+let update_sigma_univs ugraph evd =
+  { evd with universes = UState.update_sigma_univs evd.universes ugraph }
 
 exception UniversesDiffer = UState.UniversesDiffer
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 5c7a529b9c..9dc106a3d7 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -660,7 +660,8 @@ val fix_undefined_variables : evar_map -> evar_map
 (** Universe minimization *)
 val minimize_universes : evar_map -> evar_map
 
-val update_sigma_env : evar_map -> env -> evar_map
+(** Lift [UState.update_sigma_univs] *)
+val update_sigma_univs : UGraph.t -> evar_map -> evar_map
 
 (** Polymorphic universes *)
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 2fc5ade0d2..5b0e6f5785 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1037,8 +1037,8 @@ module Unsafe = struct
   let mark_as_unresolvables p evs =
     { p with solution = mark_in_evm ~goal:false p.solution evs }
 
-  let update_sigma_env pv env =
-    { pv with solution = Evd.update_sigma_env pv.solution env }
+  let update_sigma_univs ugraph pv =
+    { pv with solution = Evd.update_sigma_univs ugraph pv.solution }
 
 end
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 8853013a84..db6509c84e 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -500,8 +500,8 @@ module Unsafe : sig
   val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list ->
     Proofview_monad.goal_with_state list
 
-  (** [update_sigma_env] lifts [Evd.update_sigma_env] to the proofview *)
-  val update_sigma_env : proofview -> Environ.env -> proofview
+  (** [update_sigma_univs] lifts [UState.update_sigma_univs] to the proofview *)
+  val update_sigma_univs : UGraph.t -> proofview -> proofview
 
 end
 
diff --git a/engine/uState.ml b/engine/uState.ml
index ca0a21acf7..8d1584cd95 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -568,8 +568,8 @@ let emit_side_effects eff u =
   let u = demote_seff_univs (fst uctx) u in
   merge_seff u uctx
 
-let update_sigma_env uctx env =
-  let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) (Environ.universes env) in
+let update_sigma_univs uctx ugraph =
+  let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) ugraph in
   let eunivs =
     { uctx with
       initial_universes = univs;
diff --git a/engine/uState.mli b/engine/uState.mli
index 607c6c9452..7fec03e3b2 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -185,7 +185,7 @@ val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
 
 (** {5 TODO: Document me} *)
 
-val update_sigma_env : t -> Environ.env -> t
+val update_sigma_univs : t -> UGraph.t -> t
 
 (** {5 Pretty-printing} *)