Module `Egramml`

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

val declare_vernac_command_grammar : allow_override:bool -> Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Entry.t option -> Vernacexpr.vernac_expr grammar_prod_item list -> unit
val extend_vernac_command_grammar : undoable:bool -> Vernacexpr.extend_name -> unit
val grammar_extend : ?⁠plugin_uid:(string * string) -> 'a Pcoq.Entry.t -> 'a Pcoq.extend_statement -> unit
val get_extend_vernac_rule : Vernacexpr.extend_name -> Vernacexpr.vernac_expr grammar_prod_item list
val 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 Pcoq.Production.t