Record.RecordEntrytype one_ind_info = {inhabitant_id : Names.Id.t; |
default_dep_elim : DeclareInd.default_dep_elim; |
implfs : Impargs.manual_implicits list; |
fieldlocs : Loc.t option list; |
}type t = {global_univs : Univ.ContextSet.t; |
ubinders : UState.named_universes_entry; |
mie : Entries.mutual_inductive_entry; |
ind_infos : one_ind_info list; |
param_impls : Impargs.manual_implicits; |
}