+let universe_eq a b =
+ match a,b with
+ | [(false,_)], [(false,_)] -> universe_leq b a && universe_leq a b
+ | _, [(false,_)]
+ | [(false,_)],_ -> false
+ | _ ->
+ raise (BadConstraint
+ (lazy "trying to check if two inferred universes are equal"))
+;;
+
+let pp_constraint b x y =
+ NUri.name_of_uri x ^ (if b then " < " else " <= ") ^ NUri.name_of_uri y
+;;
+
+let pp_constraints () =
+ String.concat "\n" (List.map (fun (b,x,y) -> pp_constraint b x y) !le_constraints)
+;;
+
+let universes = ref [];;