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
---
 proofs/proof.ml  | 4 ++--
 proofs/proof.mli | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

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