Module Egramml
Mapping of grammar productions to camlp5 actions.
type 's grammar_prod_item=|GramTerminal of string|GramNonTerminal : ('a Genarg.raw_abstract_argument_type * ('s, _, 'a) Extend.symbol) 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 -> unitval get_extend_vernac_rule : Vernacexpr.extend_name -> Vernacexpr.vernac_expr grammar_prod_item listval proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type
val make_rule : (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> 'a grammar_prod_item list -> 'a Extend.production_rule