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 +++++++++
 pretyping/evd.mli | 2 ++
 2 files changed, 11 insertions(+)

(limited to 'pretyping')

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 =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 3c16b27ad9..671d62021a 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -560,6 +560,8 @@ val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_sub
 
 val nf_constraints : evar_map -> evar_map
 
+val update_sigma_env : evar_map -> env -> evar_map
+
 (** Polymorphic universes *)
 
 val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
-- 
cgit v1.2.3