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
---
 engine/evd.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/evd.ml')

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