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