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.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping/evd.mli')

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