diff options
| author | Matthieu Sozeau | 2015-07-07 16:02:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-07-07 16:02:13 +0200 |
| commit | 6f2db13c8677fd0148279483359e75b9f128aebc (patch) | |
| tree | 36be29c4dd15dfb72a0f4f18d04ebd38ca5a9098 | |
| parent | 2a28c677c3c205ff453b7b5903e4c22f4de2649b (diff) | |
Univs/minimization: Fix unused variable bug.
| -rw-r--r-- | library/universes.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/library/universes.ml b/library/universes.ml index a3926bc6f2..1c8a5ad77d 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -723,7 +723,10 @@ let pr_constraints_map cmap = prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl () ++ acc) cmap (mt ()) - + +let remove_alg l (ctx, us, algs, insts, cstrs) = + (ctx, us, LSet.remove l algs, insts, cstrs) + let minimize_univ_variables ctx us algs left right cstrs = let left, lbounds = Univ.LMap.fold (fun r lower (left, lbounds as acc) -> @@ -767,8 +770,8 @@ let minimize_univ_variables ctx us algs left right cstrs = if not (Level.equal l u) then (* Should check that u does not have upper constraints that are not already in right *) - let acc' = (ctx', us, LSet.remove l algs, insts, cstrs) in - instantiate_with_lbound u lbound false false acc + let acc' = remove_alg l acc in + instantiate_with_lbound u lbound false false acc' else acc, (true, false, lbound) | None -> try |