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

Sourcemodule Detype : sig ... end

Sourcemodule Extern : sig ... end

Sourcetype t = {

}

Combined detyping and extern flags.

Sourceval make_raw : t -> t

Sourceval current : unit -> t

Sourceval current_ignore_raw : unit -> t

Sourceval print_universes : bool ref

The following flag is still accessed directly, but not when printing constr.

module PrintingInductiveMake
  (_ : sig ... end) : 
  Goptions.RefConvertArg
    with type t = Names.inductive
     and module Set = Names.Indset_env

Sourceval set_extern_depth : int option -> unit