package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

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