diff options
| author | Matthieu Sozeau | 2015-03-17 18:44:23 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-03-17 18:44:23 +0100 |
| commit | adb721441e9ff9bf7cdb1b4603628d95ca1f016a (patch) | |
| tree | da10d09179338729799ba253c6ac2e30b8dfbaf5 /pretyping/evd.mli | |
| parent | 4d95eb4e878f375a69f1b48d8833801bf555fdd0 (diff) | |
Add function to fix the non-substituted universe variables of an evar_map.
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 0765b951fd..fe785a8314 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -530,6 +530,8 @@ val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> e val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val abstract_undefined_variables : evar_universe_context -> evar_universe_context +val fix_undefined_variables : evar_map -> evar_map + val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst val nf_constraints : evar_map -> evar_map |