package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'s0 grammar_prod_item =
  1. | GramTerminal of string
  2. | GramNonTerminal : ('a Genarg.raw_abstract_argument_type * ('s, 'b, '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
val make_rule : (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> 'a grammar_prod_item list -> 'a Pcoq.Production.t