Module Indtypes
val check_inductive : Environ.env -> sec_univs:UVars.Instance.t option -> Names.MutInd.t -> Entries.mutual_inductive_entry -> Declarations.mutual_inductive_bodyCheck an inductive.
Indtypesval check_inductive : Environ.env -> sec_univs:UVars.Instance.t option -> Names.MutInd.t -> Entries.mutual_inductive_entry -> Declarations.mutual_inductive_bodyCheck an inductive.