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