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

5 files changed, 18 insertions, 14 deletions

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