diff options
| author | Matthieu Sozeau | 2014-05-30 21:55:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-04 15:48:31 +0200 |
| commit | 86c6649382bb9e42281ffe956c627c6d3987559b (patch) | |
| tree | 7d42f94d33c2ac2e4241ce92014abc0785aed6ca /pretyping | |
| parent | dd96b1e5e8d0eb9f93cff423b6f9cf900aee49d7 (diff) | |
- Force every universe level to be >= Prop, so one cannot "go under" it anymore.
- Finish the change to level-to-level substitutions, in the checker.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index e8b360b86f..038b91ec61 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -436,9 +436,8 @@ let process_universe_constraints univs vars alg templ cstrs = instantiate_variable r' l vars else if not (Univ.check_eq univs l r) then (* Two rigid/global levels, none of them being local, - one of them being Prop, disallow *) - if Univ.Level.equal l' Univ.Level.prop || - Univ.Level.equal r' Univ.Level.prop then + one of them being Prop/Set, disallow *) + if Univ.Level.is_small l' || Univ.Level.is_small r' then raise (Univ.UniverseInconsistency (Univ.Eq, l, r, [])) else if fo then @@ -1013,7 +1012,8 @@ let uctx_new_univ_variable template rigid name | Some n -> UNameMap.add n u uctx.uctx_names | None -> uctx.uctx_names in - {uctx'' with uctx_names = names; uctx_local = ctx'}, u + {uctx'' with uctx_names = names; uctx_local = ctx'; + uctx_universes = Univ.add_universe u uctx.uctx_universes}, u let new_univ_level_variable ?(template=false) ?name rigid evd = let uctx', u = uctx_new_univ_variable template rigid name evd.universes in |