diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-01 15:19:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-09 16:30:11 +0100 |
| commit | d640b676282285d52ac19038d693080e64eb5ea7 (patch) | |
| tree | 6c09e0963369997ff5e9c55490ff98a04331d1cd /engine/evd.ml | |
| parent | ee7f5486fff86c453767997f97eda381983c4bbc (diff) | |
Statically enforce that ULub is only between levels.
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index b7b87370e..f6e13e1f4 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -857,15 +857,10 @@ let set_eq_sort env d s1 s2 = | Some (u1, u2) -> if not (type_in_type env) then add_universe_constraints d - (Universes.Constraints.singleton (u1,Universes.UEq,u2)) + (Universes.Constraints.singleton (Universes.UEq (u1,u2))) else d -let has_lub evd u1 u2 = - if Univ.Universe.equal u1 u2 then evd - else add_universe_constraints evd - (Universes.Constraints.singleton (u1,Universes.ULub,u2)) - let set_eq_level d u1 u2 = add_constraints d (Univ.enforce_eq_level u1 u2 Univ.Constraint.empty) @@ -883,7 +878,7 @@ let set_leq_sort env evd s1 s2 = | None -> evd | Some (u1, u2) -> if not (type_in_type env) then - add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2)) + add_universe_constraints evd (Universes.Constraints.singleton (Universes.ULe (u1,u2))) else evd let check_eq evd s s' = |