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.