package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Mapping of grammar productions to camlp5 actions.

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

type 's grammar_prod_item =
  1. | GramTerminal of string
  2. | GramNonTerminal : ('a Genarg.raw_abstract_argument_type * ('s, _, 'a) Pcoq.Symbol.t) Loc.located -> 's grammar_prod_item
val extend_vernac_command_grammar : Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Entry.t option -> Vernacexpr.vernac_expr grammar_prod_item list -> unit
val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type

Utility function reused in Egramcoq :

val make_rule : (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> 'a grammar_prod_item list -> 'a Pcoq.Production.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct