package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b
doc/coq-core.vernac/Egramml/index.html
Module EgrammlSource
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.
Source
type 's grammar_prod_item = | GramTerminal of string| GramNonTerminal : ('a Genarg.raw_abstract_argument_type * ('s, _, 'a) Pcoq.Symbol.t) Loc.located -> 's grammar_prod_item
Source
val extend_vernac_command_grammar :
Vernacexpr.extend_name ->
Vernacexpr.vernac_expr Pcoq.Entry.t option ->
Vernacexpr.vernac_expr grammar_prod_item list ->
unitSource
val get_extend_vernac_rule :
Vernacexpr.extend_name ->
Vernacexpr.vernac_expr grammar_prod_item listUtility function reused in Egramcoq :
Source
val make_rule :
(Loc.t -> Genarg.raw_generic_argument list -> 'a) ->
'a grammar_prod_item list ->
'a Pcoq.Production.t