+let inf ~strict l = inf ~strict (family_of l) l;;
+
+let rec universe_lt a b =
+ match a, b with
+ | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
+ | l, ([((`Type|`CProp),b)] as orig_b) ->
+ List.for_all
+ (function
+ | `Succ,_ as a ->
+ (match sup [a] with
+ | None -> false
+ | Some x -> universe_lt x orig_b)
+ | _, a -> lt_path a b) l
+ | _, ([] | [`Succ,_] | _::_::_) ->
+ raise (BadConstraint (lazy (
+ "trying to check if "^string_of_univ a^
+ " is lt than the inferred universe " ^ string_of_univ b)))
+;;
+
+
+let allowed_sort_elimination s1 s2 =
+ match s1, s2 with
+ | C.Type (((`Type|`Succ),_)::_ | []), C.Type (((`Type|`Succ),_)::_ | [])
+ | C.Type _, C.Type ((`CProp,_)::_)
+ | C.Type _, C.Prop
+ | C.Prop, C.Prop -> `Yes
+
+ | C.Type ((`CProp,_)::_), C.Type (((`Type|`Succ),_)::_ | [])
+ | C.Prop, C.Type _ -> `UnitOnly
+;;