package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Coq_checklib.CheckInductive`Source

Sourcetype ind_retroknowledge = (int * CPrimitives.prim_ind_ex) option

Sourceexception 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