From adb721441e9ff9bf7cdb1b4603628d95ca1f016a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 17 Mar 2015 18:44:23 +0100 Subject: Add function to fix the non-substituted universe variables of an evar_map. --- pretyping/evd.ml | 12 ++++++++++++ pretyping/evd.mli | 2 ++ 2 files changed, 14 insertions(+) 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 -- cgit v1.2.3