Indtypes
val check_inductive : Environ.env -> sec_univs:UVars.Instance.t option -> Names.MutInd.t -> Entries.mutual_inductive_entry -> Declarations.mutual_inductive_body * IndTyping.NotPrimRecordReason.t option
Check an inductive.