Egramml (coq-core.Egramml)

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

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

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