diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-03-23 13:10:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-03-23 13:10:34 +0100 |
| commit | 224d3b0e8be9b6af8194389141c9508504cf887c (patch) | |
| tree | e36a175c48d3b7c6bdd10eb9907f726af7f3a9e7 /engine | |
| parent | 690ac9fe35ff153a2348b64984817cb37b7764e4 (diff) | |
| parent | 3646aea90ae927af9262e994048a3bd863c57839 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 12 | ||||
| -rw-r--r-- | engine/evd.mli | 2 |
2 files changed, 14 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 454c51195..bf519fb7c 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 diff --git a/engine/evd.mli b/engine/evd.mli index 0765b951f..fe785a831 100644 --- a/engine/evd.mli +++ b/engine/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 |