From 576c1153dae2b3660d35127862aeb3d528eb6d8d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 25 Aug 2020 12:02:35 +0200
Subject: 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
---
 stm/stm.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'stm')

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 =
-- 
cgit v1.2.3