diff options
| author | Matthieu Sozeau | 2014-04-07 12:53:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:58 +0200 |
| commit | 105db906ae45e792d1caeeb2e3fb7f69944b2caa (patch) | |
| tree | b12ca28e6b172d2524c6a11c851c7d568f6a2411 /pretyping/evd.ml | |
| parent | b17c1e128fad2e84ebe4e4742b47bd67d88c56d6 (diff) | |
- Fixes for canonical structure resolution (check that the initial term indeed unifies
with the projected term, keeping track of universes).
- Fix the [unify] tactic to fail properly.
- Fix unification to disallow lowering a global Type(i) universe to Prop or Set.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index d185685005..166bab4b82 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -390,19 +390,20 @@ let process_universe_constraints univs vars alg local cstrs = instantiate_variable l' (Univ.Universe.make r') vars else if rloc then instantiate_variable r' (Univ.Universe.make l') vars - else - (* Two rigid/global levels, one of them being Prop/Set, disallow *) - (* if Univ.is_small_univ l' || Univ.is_small_univ r' then *) - (* raise UniversesDiffer *) - (* else *) - if fo then - if not (Univ.check_eq univs l r) then + else if not (Univ.check_eq univs l r) then + (* Two rigid/global levels, none of them being local, + 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 raise UniversesDiffer in Univ.enforce_eq_level l' r' local | _, _ (* One of the two is algebraic or global *) -> if Univ.check_eq univs l r then local - else raise UniversesDiffer + else + raise UniversesDiffer in let local = Univ.UniverseConstraints.fold (fun (l,d,r) local -> unify_universes false l d r local) |