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=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

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