Record.Record_decl
A record is an inductive mie with extra metadata
mie
type t = {
entry : RecordEntry.t;
records : Data.t list;
projections_kind : Decls.definition_object_kind;
indlocs : DeclareInd.indlocs;
}