diff options
| author | Matthieu Sozeau | 2015-10-29 15:11:29 -0400 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-29 15:18:16 -0400 |
| commit | a3a17b514a2ffaba54cd182fdf27b7e84366ab44 (patch) | |
| tree | 8d48786996f4a8217404fbd43f3fdc72f922592f /pretyping | |
| parent | 78edfe09f34db4a28fb41a1f6fd3bb4922d09ec8 (diff) | |
Handle side-effects of Vernacular commands inside proofs better, so that
universes are declared correctly in the enclosing proofs evar_map's.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 9 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 |
2 files changed, 11 insertions, 0 deletions
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 |