From d640b676282285d52ac19038d693080e64eb5ea7 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 1 Mar 2018 15:19:52 +0100 Subject: Statically enforce that ULub is only between levels. --- engine/evd.ml | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) (limited to 'engine/evd.ml') 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' = -- cgit v1.2.3