+let universe_leq a b =
+ match a, b with
+ | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
+ | l, [((`Type|`CProp),b)] ->
+ List.for_all
+ (function
+ | `Succ,a -> lt_path a b
+ | _, a -> NUri.eq a b || lt_path a b) l
+ | _, ([] | [`Succ,_] | _::_::_) ->
+ raise (BadConstraint (lazy (
+ "trying to check if "^string_of_univ a^
+ " is leq than the inferred universe " ^ string_of_univ b)))
+;;
+
+let are_sorts_convertible ~test_eq_only s1 s2 =
+ match s1,s2 with
+ | C.Type a, C.Type b when not test_eq_only -> universe_leq a b
+ | C.Type a, C.Type b -> universe_eq a b
+ | C.Prop,C.Type _ -> (not test_eq_only)
+ | C.Prop, C.Prop -> true
+ | _ -> false
+;;
+
+let pp_constraint x y =
+ NUri.name_of_uri x ^ " < " ^ NUri.name_of_uri y