Module ComInductive.Mind_decl

type t = {
mie : Entries.mutual_inductive_entry;
nuparams : int option;
univ_binders : UnivNames.universe_binders;
implicits : DeclareInd.one_inductive_impls list;
uctx : Univ.ContextSet.t;
where_notations : Metasyntax.where_decl_notation list;
coercions : Libnames.qualid list;
}

inductive_expr at the constr level