From bc0246f5a570f70c7befb150d7b544032acbaf7e Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 3 Mar 2018 23:59:48 +0100 Subject: 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. --- engine/universes.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'engine') 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 -- cgit v1.2.3