diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-05-31 00:45:41 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-29 11:52:52 +0200 |
| commit | 307d0cbfded6fbfa2b82b38e43f90a51caf0eb80 (patch) | |
| tree | 14ae63001df05624057a4e777107e5083e6e5b8c /library | |
| parent | c200c2b41e88dd7d4a1b9e90e0c35a7ed047309c (diff) | |
universes.ml: Minor code cleanup
Diffstat (limited to 'library')
| -rw-r--r-- | library/universes.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/library/universes.ml b/library/universes.ml index 75cbd5604..21d960ea3 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -926,9 +926,7 @@ let normalize_context_set ctx us algs = mentionning other variables remain in noneqs. *) let noneqs, ucstrsl, ucstrsr = Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> - let lus = LMap.mem l us - and rus = LMap.mem r us - in + let lus = LMap.mem l us and rus = LMap.mem r us in let ucstrsl' = if lus then add_list_map l (d, r) ucstrsl else ucstrsl @@ -1090,13 +1088,6 @@ let solve_constraints_system levels level_bounds level_min = for j=0 to nind-1 do if not (Int.equal i j) && Int.Set.mem j clos.(i) then (v.(i) <- Universe.sup v.(i) level_bounds.(j)); - (* level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) *) done; - (* for j=0 to nind-1 do *) - (* match levels.(j) with *) - (* | Some u when not (Univ.Level.is_small u) -> *) - (* v.(i) <- univ_level_rem u v.(i) level_min.(i) *) - (* | _ -> () *) - (* done *) done; v |