Module `Indtypes`

val check_inductive : Environ.env -> Names.MutInd.t -> Entries.mutual_inductive_entry -> Declarations.mutual_inductive_body: Check an inductive.

type inductive_error = | NonPos of Environ.env * Constr.constr * Constr.constr | NotEnoughArgs of Environ.env * Constr.constr * Constr.constr | NotConstructor of Environ.env * Names.Id.t * Constr.constr * Constr.constr * int * int | NonPar of Environ.env * Constr.constr * int * Constr.constr * Constr.constr | SameNamesTypes of Names.Id.t | SameNamesConstructors of Names.Id.t | SameNamesOverlap of Names.Id.t list | NotAnArity of Environ.env * Constr.constr | BadEntry | LargeNonPropInductiveNotInType | BadUnivs: Deprecated