CheckInductive (rocq-runtime.Coq_checklib.CheckInductive)

type ind_retroknowledge = (int * CPrimitives.prim_ind_ex) option

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 ->
  ind_retroknowledge ->
  Environ.env