Record.Record_declA record is an inductive mie with extra metadata in records
type t = {mie : Entries.mutual_inductive_entry; |
records : Data.t list; |
primitive_proj : bool; |
impls : DeclareInd.one_inductive_impls list; |
globnames : UState.named_universes_entry; |
global_univ_decls : Univ.ContextSet.t option; |
projunivs : Entries.universes_entry; |
ubinders : UnivNames.universe_binders; |
projections_kind : Decls.definition_object_kind; |
poly : bool; |
}