+let string_of_univ u =
+ let b = Buffer.create 100 in
+ let f = Format.formatter_of_buffer b in
+ ppsort f (NCic.Type u);
+ Format.fprintf f "@?";
+ Buffer.contents b
+;;
+
+let eq_univ (b1,u1) (b2,u2) = b1=b2 && NUri.eq u1 u2;;
+
+let max (l1:NCic.universe) (l2:NCic.universe) =
+ match l2 with
+ | x::tl ->
+ let rest = List.filter (fun y -> not (eq_univ x y)) (l1@tl) in
+ x :: HExtlib.list_uniq ~eq:eq_univ
+ (List.sort (fun (b1,u1) (b2,u2) ->
+ let res = compare b1 b2 in
+ if res = 0 then NUri.compare u1 u2 else res)
+ rest)
+ | [] ->
+ match l1 with
+ | [] -> []
+ | ((`Type|`Succ), _)::_ -> l1
+ | (`CProp, u)::tl -> (`Type, u)::tl
+;;
+
+let lt_constraints = ref [] (* a,b := a < b *)
+
+let rec lt_path_uri avoid a b =
+ List.exists
+ (fun (x,y) ->
+ NUri.eq y b &&
+ (NUri.eq a x ||
+ (not (List.exists (NUri.eq x) avoid) &&
+ lt_path_uri (x::avoid) a x))
+ ) !lt_constraints
+;;
+
+let lt_path a b = lt_path_uri [b] a b;;
+
+let universe_eq a b =
+ match a,b with
+ | [(`Type|`CProp) as b1, u1], [(`Type|`CProp) as b2, u2] ->
+ b1 = b2 && NUri.eq u1 u2
+ | _, [(`Type|`CProp),_]
+ | [(`Type|`CProp),_],_ -> false
+ | _ ->
+ raise (BadConstraint
+ (lazy "trying to check if two inferred universes are equal"))
+;;