diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-11-14 11:50:04 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:55 +0200 |
| commit | c1cd47d5dff18f12af063d2c8defbd985c97dec6 (patch) | |
| tree | e459818ae127339883bb124a525191215a3b38f2 /library/universes.ml | |
| parent | 28e5f4def8bebdaf3bd75b6662bbd4fd88594689 (diff) | |
- Fix comparison of universes.
- Shortcut for Set <= x checks, assuming that this is always true except when
x (or rather its canonical representative) is Prop. Invariant to check.
- Uncomment the profiling code and make it depend on a (statically known) boolean.
Diffstat (limited to 'library/universes.ml')
| -rw-r--r-- | library/universes.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/library/universes.ml b/library/universes.ml index b31aab198..99c8b39f9 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -638,6 +638,9 @@ let restrict_universe_context (univs,csts) s = csts Constraint.empty in (univs', csts') +let is_small_leq (l,d,r) = + Level.is_small l && d == Univ.Le + let is_prop_leq (l,d,r) = Level.equal Level.prop l && d == Univ.Le @@ -651,7 +654,7 @@ let refresh_constraints univs (ctx, cstrs) = let cstrs', univs' = Univ.Constraint.fold (fun c (cstrs', univs as acc) -> let c = translate_cstr c in - if Univ.check_constraint univs c && not (is_prop_leq c) then acc + if Univ.check_constraint univs c && not (is_small_leq c) then acc else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs)) cstrs (Univ.Constraint.empty, univs) in ((ctx, cstrs'), univs') |