From a3a17b514a2ffaba54cd182fdf27b7e84366ab44 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 29 Oct 2015 15:11:29 -0400
Subject: Handle side-effects of Vernacular commands inside proofs better, so
 that universes are declared correctly in the enclosing proofs evar_map's.

---
 pretyping/evd.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'pretyping/evd.ml')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 36d9c25fdd..db6b366b75 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1358,6 +1358,15 @@ let add_universe_name evd s l =
 
 let universes evd = evd.universes.uctx_universes
 
+let update_sigma_env evd env =
+  let univs = Environ.universes env in
+  let eunivs =
+    { evd.universes with uctx_initial_universes = univs;
+			 uctx_universes = univs }
+  in
+  let eunivs = merge_uctx true univ_rigid eunivs eunivs.uctx_local in
+  { evd with universes = eunivs }
+
 (* Conversion w.r.t. an evar map and its local universes. *)
 
 let conversion_gen env evd pb t u =
-- 
cgit v1.2.3