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/Egramml/index.html

Module EgrammlSource

Mapping of grammar productions to camlp5 actions.

This is the part specific to vernac extensions. For the Rocq-level Notation and Tactic Notation, see Egramrocq.

Sourcetype 's grammar_prod_item =
  1. | GramTerminal of string
  2. | GramNonTerminal : ('a Genarg.raw_abstract_argument_type * ('s, _, 'a) Procq.Symbol.t) Loc.located -> 's grammar_prod_item
Sourceval declare_vernac_command_grammar : allow_override:bool -> Vernacexpr.extend_name -> Vernacexpr.vernac_expr Procq.Entry.t option -> Vernacexpr.vernac_expr grammar_prod_item list -> unit
Sourceval extend_vernac_command_grammar : undoable:bool -> Vernacexpr.extend_name -> unit
Sourceval grammar_extend : ?plugin_uid:(string * string) -> 'a Procq.Entry.t -> 'a Procq.extend_statement -> unit
Sourceval proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type

Utility function reused in Egramrocq :

Sourceval make_rule : (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> 'a grammar_prod_item list -> 'a Procq.Production.t