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

15 files changed, 45 insertions, 33 deletions

diff --git a/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh
new file mode 100644
index 0000000000..f0878202d3
--- /dev/null
+++ b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "12892" ] || [ "$CI_BRANCH" = "update-s-univs" ]; then
+
+    elpi_CI_REF=update-s-univs
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    equations_CI_REF=update-s-univs
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+fi
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} *)
 
diff --git a/proofs/proof.ml b/proofs/proof.ml
index d7904c56a8..616cbf9678 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -353,8 +353,8 @@ let compact p =
   let entry, proofview = Proofview.compact p.entry p.proofview in
   { p with proofview; entry }
 
-let update_sigma_env p env =
-  let proofview = Proofview.Unsafe.update_sigma_env p.proofview env in
+let update_sigma_univs ugraph p =
+  let proofview = Proofview.Unsafe.update_sigma_univs ugraph p.proofview in
   { p with proofview }
 
 (*** Function manipulation proof extra informations ***)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index a0d4759bfc..ffb8380147 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -76,8 +76,8 @@ val partial_proof : t -> EConstr.constr list
 
 val compact : t -> t
 
-(** [update_sigma_env] lifts [Evd.update_sigma_env] to the proof *)
-val update_sigma_env : t -> Environ.env -> t
+(** [update_sigma_univs] lifts [UState.update_sigma_univs] to the proof *)
+val update_sigma_univs : UGraph.t -> t -> t
 
 (* Returns the proofs (with their type) of the initial goals.
     Raises [UnfinishedProof] is some goals remain to be considered.
diff --git a/stm/stm.ml b/stm/stm.ml
index 9999e66c45..4ca0c365bf 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -142,10 +142,6 @@ let may_pierce_opaque = function
   | VernacExtend (("ExtractionInductive",_), _) -> true
   | _ -> false
 
-let update_global_env () =
-  if PG_compat.there_are_pending_proofs () then
-    PG_compat.update_global_env ()
-
 module Vcs_ = Vcs.Make(Stateid.Self)
 type future_proof = Declare.Proof.closed_proof_output Future.computation
 
@@ -2336,7 +2332,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
   let inject_non_pstate (s,l) =
-    Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env ()
+    Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l;
+    if PG_compat.there_are_pending_proofs () then
+      PG_compat.update_sigma_univs (Global.universes ())
   in
 
   let rec pure_cherry_pick_non_pstate safe_id id =
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 28e6f21d41..49eb627c4d 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1734,8 +1734,8 @@ let return_proof ps =
   let p, uctx = prepare_proof ~unsafe_typ:false ps in
   List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx
 
-let update_global_env =
-  map ~f:(fun p -> Proof.update_sigma_env p (Global.env ()))
+let update_sigma_univs ugraph p =
+  map ~f:(Proof.update_sigma_univs ugraph) p
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
@@ -2251,7 +2251,7 @@ let rec solve_obligation prg num tac =
   let scope = Locality.Global Locality.ImportNeedQualified in
   let kind = kind_of_obligation (snd obl.obl_status) in
   let evd = Evd.from_ctx (Internal.get_uctx prg) in
-  let evd = Evd.update_sigma_env evd (Global.env ()) in
+  let evd = Evd.update_sigma_univs (Global.universes ()) evd in
   let auto ~pm n oblset tac = auto_solve_obligations ~pm n ~oblset tac in
   let proof_ending =
     let name = Internal.get_name prg in
@@ -2292,7 +2292,7 @@ and solve_obligation_by_tac prg obls i tac =
             | None -> !default_tactic
         in
         let uctx = Internal.get_uctx prg in
-        let uctx = UState.update_sigma_env uctx (Global.env ()) in
+        let uctx = UState.update_sigma_univs uctx (Global.universes ()) in
         let poly = Internal.get_poly prg in
         match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac ~poly ~uctx with
         | None -> None
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 3001d0d206..1ad79928d5 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -246,10 +246,10 @@ module Proof : sig
 
   val compact : t -> t
 
-  (** Update the proofs global environment after a side-effecting command
-      (e.g. a sublemma definition) has been run inside it. Assumes
-      there_are_pending_proofs. *)
-  val update_global_env : t -> t
+  (** Update the proof's universe information typically after a
+      side-effecting command (e.g. a sublemma definition) has been run
+      inside it. *)
+  val update_sigma_univs : UGraph.t -> t -> t
 
   val get_open_goals : t -> int
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 6be2fb0d43..edf48fef1a 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -211,8 +211,11 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
     (fun ~st ->
        let before_univs = Global.universes () in
        let pstack, pm = interp_expr ~atts:cmd.attrs ~st cmd.expr in
-       if before_univs == Global.universes () then pstack, pm
-       else Option.map (Vernacstate.LemmaStack.map_top ~f:Declare.Proof.update_global_env) pstack, pm)
+       let after_univs = Global.universes () in
+       if before_univs == after_univs then pstack, pm
+       else
+         let f = Declare.Proof.update_sigma_univs after_univs in
+         Option.map (Vernacstate.LemmaStack.map ~f) pstack, pm)
     ~st
 
 (* XXX: This won't properly set the proof mode, as of today, it is
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 6d12d72408..204008997d 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -80,7 +80,7 @@ module LemmaStack = struct
 
   type t = Declare.Proof.t * Declare.Proof.t list
 
-  let map f (pf, pfl) = (f pf, List.map f pfl)
+  let map ~f (pf, pfl) = (f pf, List.map f pfl)
   let map_top ~f (pf, pfl) = (f pf, pfl)
 
   let pop (ps, p) = match p with
@@ -96,7 +96,7 @@ module LemmaStack = struct
 
   let get_all_proof_names (pf : t) =
     let prj x = Declare.Proof.get x in
-    let (pn, pns) = map Proof.(function pf -> (data (prj pf)).name) pf in
+    let (pn, pns) = map ~f:Proof.(function pf -> (data (prj pf)).name) pf in
     pn :: pns
 
   let copy_info src tgt =
@@ -218,7 +218,7 @@ module Declare_ = struct
                   Declare.Proof.info pt)
 
   let discard_all () = s_lemmas := None
-  let update_global_env () = dd (Declare.Proof.update_global_env)
+  let update_sigma_univs ugraph = dd (Declare.Proof.update_sigma_univs ugraph)
 
   let get_current_context () = cc Declare.Proof.get_current_context
 
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 5efdb3cc68..e1b13dcb73 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -40,6 +40,7 @@ module LemmaStack : sig
   val pop : t -> Declare.Proof.t * t option
   val push : t option -> Declare.Proof.t -> t
 
+  val map : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t
   val map_top : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t
   val with_top : t -> f:(Declare.Proof.t -> 'a ) -> 'a
 
@@ -112,7 +113,7 @@ module Declare : sig
   val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof
 
   val discard_all : unit -> unit
-  val update_global_env : unit -> unit
+  val update_sigma_univs : UGraph.t -> unit
 
   val get_current_context : unit -> Evd.evar_map * Environ.env