diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-30 18:32:23 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:12 +0200 |
| commit | 62e6f7e37512e523eafe65e6a58369361e74d4d5 (patch) | |
| tree | 2579607e7b3930267bcedfc962dd2c76bbee9119 | |
| parent | 42dd4e73346e29db2fe586234b00ca79bd207a5a (diff) | |
Univs: fix minimization to allow lowering a universe to Set, not Prop.
| -rw-r--r-- | library/universes.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/library/universes.ml b/library/universes.ml index 0133f5deb..9bc21b0e5 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -834,8 +834,10 @@ let normalize_context_set ctx us algs = if Univ.Level.is_small l then (Constraint.add cstr smallles, noneqs) else if Level.is_small r then - raise (Univ.UniverseInconsistency - (Le,Universe.make l,Universe.make r,None)) + if Level.is_prop r then + raise (Univ.UniverseInconsistency + (Le,Universe.make l,Universe.make r,None)) + else (smallles, Constraint.add (l,Eq,r) noneqs) else (smallles, Constraint.add cstr noneqs) else (smallles, Constraint.add cstr noneqs)) csts (Constraint.empty, Constraint.empty) @@ -850,13 +852,13 @@ let normalize_context_set ctx us algs = Univ.Constraint.fold (fun (l, d, r) g -> let g = if not (Level.is_small l || LSet.mem l ctx) then - try Univ.add_universe l true g + try Univ.add_universe l false g with Univ.AlreadyDeclared -> g else g in let g = if not (Level.is_small r || LSet.mem r ctx) then - try Univ.add_universe r true g + try Univ.add_universe r false g with Univ.AlreadyDeclared -> g else g in g) csts g |