diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-17 18:44:23 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-03-17 18:44:23 +0100 |
| commit | adb721441e9ff9bf7cdb1b4603628d95ca1f016a (patch) | |
| tree | da10d09179338729799ba253c6ac2e30b8dfbaf5 | |
| parent | 4d95eb4e878f375a69f1b48d8833801bf555fdd0 (diff) | |
Add function to fix the non-substituted universe variables of an evar_map.
| -rw-r--r-- | pretyping/evd.ml | 12 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 |
2 files changed, 14 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 454c51195..bf519fb7c 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1189,6 +1189,18 @@ let abstract_undefined_variables uctx = in { uctx with uctx_local = Univ.ContextSet.empty; uctx_univ_algebraic = vars' } +let fix_undefined_variables ({ universes = uctx } as evm) = + let algs', vars' = + Univ.LMap.fold (fun u v (algs, vars as acc) -> + if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars) + else acc) + uctx.uctx_univ_variables + (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables) + in + {evm with universes = + { uctx with uctx_univ_variables = vars'; + uctx_univ_algebraic = algs' } } + let refresh_undefined_univ_variables uctx = let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 0765b951f..fe785a831 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 |