ComInductive.Internal
val compute_constructor_level : Environ.env -> Evd.evar_map -> EConstr.rel_context -> Sorts.t