ComInductive.Mind_decltype t = {mie : Entries.mutual_inductive_entry; |
default_dep_elim : DeclareInd.default_dep_elim list; |
nuparams : int option; |
univ_binders : UnivNames.universe_binders; |
implicits : DeclareInd.one_inductive_impls list; |
uctx : Univ.ContextSet.t; |
where_notations : Metasyntax.notation_interpretation_decl list; |
coercions : Libnames.qualid list; |
indlocs : Loc.t option list; |
}inductive_expr at the constr level