+let cache = NUri.UriHash.create 313;;
+let history = ref [];;
+let frozen_list = ref [];;
+
+let get_obj = ref (fun _ -> assert false);;
+let set_get_obj f = get_obj := f;;
+
+let type0 = []
+
+module F = Format
+
+let rec ppsort f = function
+ | C.Prop -> F.fprintf f "Prop"
+ | (C.Type []) -> F.fprintf f "Type0"
+ | (C.Type [`Type, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
+ | (C.Type [`Succ, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
+ | (C.Type [`CProp, u]) -> F.fprintf f "P(%s)" (NUri.name_of_uri u)
+ | (C.Type l) ->
+ F.fprintf f "Max(";
+ ppsort f ((C.Type [List.hd l]));
+ List.iter (fun x -> F.fprintf f ",";ppsort f ((C.Type [x]))) (List.tl l);
+ F.fprintf f ")"
+;;
+
+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
+;;