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