Coq_checklib.CheckInductivetype ind_retroknowledge = (int * CPrimitives.prim_ind_ex) optionexception InductiveMismatch of Names.MutInd.t * stringSome field of the inductive is different from what the kernel infers.
val check_inductive : Environ.env -> Names.MutInd.t -> Declarations.mutual_inductive_body -> ind_retroknowledge -> Environ.env