diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-03 23:59:48 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-13 14:10:04 +0200 |
| commit | bc0246f5a570f70c7befb150d7b544032acbaf7e (patch) | |
| tree | b3942f3ea806b0ffc6f93a44627bf661c15af0ab /engine | |
| parent | 4baca7221917685210899b766e71782ddae4249f (diff) | |
niv minimization: remove [remove_lower] abbreviation
It's not long, used only once and it's easier to understand what it
does when it's inlined.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/universes.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index fe7f406b4..1b1ce7cec 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -788,10 +788,6 @@ let _pr_constraints_map (cmap:constraints_map) = let remove_alg l (ctx, us, algs, insts, cstrs) = (ctx, us, LSet.remove l algs, insts, cstrs) -let remove_lower u lower = - let levels = Universe.levels u in - LSet.fold (fun l acc -> LMap.remove l acc) levels lower - let minimize_univ_variables ctx us algs left right cstrs = let left, lbounds = Univ.LMap.fold (fun r lower (left, lbounds as acc) -> @@ -850,7 +846,7 @@ let minimize_univ_variables ctx us algs left right cstrs = if alg then (* u is algebraic: we instantiate it with its lower bound, if any, or enforce the constraints if it is bounded from the top. *) - let lower = remove_lower lbound lower in + let lower = LSet.fold LMap.remove (Universe.levels lbound) lower in instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc else (* u is non algebraic *) match Universe.level lbound with |