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

2 files changed, 4 insertions, 4 deletions

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.