ComInductive.Mind_decltype 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