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/evd.mli | |
| 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/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 2 |
1 files changed, 2 insertions, 0 deletions
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 |