diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 454c51195b..bf519fb7c0 100644 --- a/engine/evd.ml +++ b/engine/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 |