Module ComInductive.Internal

val inductive_levels : Environ.env -> Evd.evar_map -> EConstr.constr list -> EConstr.rel_context list list -> Evd.evar_map * EConstr.t list

Returns the modified arities (the result sort may be replaced by Prop). Should be called with minimized universes.