raise (BadConstraint
(lazy "trying to check if a universe is less or equal than an inferred universe"))
-let universe_eq a b = universe_leq b a || universe_leq a b
+let universe_eq a b = universe_leq b a && universe_leq a b
-let add_le_constraint strict a b =
+let add_constraint strict a b =
match a,b with
| [false,a2],[false,b2] ->
if not (le_path_uri [] strict a2 b2) then (