package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.vernac/Pvernac/index.html

Module PvernacSource

Sourcetype proof_mode
Sourcemodule Vernac_ : sig ... end
Sourcemodule Unsafe : sig ... end
Sourceval main_entry : proof_mode option -> Vernacexpr.vernac_control option Procq.Entry.t

The main entry: reads an optional vernac command

Grammar entry for tactics: proof mode(s). By default Coq's grammar has an empty entry (non-terminal) for tactics. A plugin can register its non-terminal by providing a name and a grammar entry.

For example the Ltac plugin register the "Classic" grammar entry for parsing its tactics.

Sourcetype proof_mode_entry =
  1. | ProofMode : {
    1. command_entry : Vernacexpr.vernac_expr Procq.Entry.t;
    2. wit_tactic_expr : ('raw, _, unit) Genarg.genarg_type;
    3. tactic_expr_entry : 'raw Procq.Entry.t;
    } -> proof_mode_entry
Sourceval register_proof_mode : string -> proof_mode_entry -> proof_mode
Sourceval lookup_proof_mode : string -> proof_mode option
Sourceval proof_mode_to_string : proof_mode -> string
Sourceval list_proof_modes : unit -> proof_mode_entry CString.Map.t
Sourceval get_default_proof_mode : unit -> proof_mode
Sourceval proof_mode_opt_name : string list