CheckInductive (rocq-runtime.Coq_checklib.CheckInductive)

exception InductiveMismatch of Names.MutInd.t * string

Some field of the inductive is different from what the kernel infers.

val check_inductive : Environ.env -> Names.MutInd.t -> Declarations.mutual_inductive_body -> Environ.env