From a970072a64348a1b5af1cd45a138da819ef0a8d2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 23 Aug 2020 17:52:15 +0200
Subject: Update sigma instead of erasing it in `update_global_env`

---
 vernac/declare.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'vernac')

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 66537c2978..28e6f21d41 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1735,11 +1735,7 @@ let return_proof ps =
   List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx
 
 let update_global_env =
-  map ~f:(fun p ->
-      let { Proof.sigma } = Proof.data p in
-      let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
-      let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in
-      p)
+  map ~f:(fun p -> Proof.update_sigma_env p (Global.env ()))
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-- 
cgit v1.2.3