coq 8.7.2 · OCaml Package

module Gram : sig ... end

val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit

val parse_string : 'a Gram.entry -> string -> 'a

val eoi_entry : 'a Gram.entry -> 'a Gram.entry

val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry

type gram_universe

val get_univ : string -> gram_universe

val uprim : gram_universe

val uconstr : gram_universe

val utactic : gram_universe

val uvernac : gram_universe

val register_grammar : 
  ('raw, 'glb, 'top) Genarg.genarg_type ->
  'raw Gram.entry ->
  unit

val genarg_grammar : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw Gram.entry

val create_generic_entry : 
  gram_universe ->
  string ->
  ('a, Genarg.rlevel) Genarg.abstract_argument_type ->
  'a Gram.entry

module Prim : sig ... end

module Constr : sig ... end

module Module : sig ... end

module Vernac_ : sig ... end

val main_entry : (Loc.t * Vernacexpr.vernac_expr) option Gram.entry

val get_command_entry : unit -> Vernacexpr.vernac_expr Gram.entry

val set_command_entry : Vernacexpr.vernac_expr Gram.entry -> unit

val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option

type gram_reinit = Extend.gram_assoc * Extend.gram_position

val grammar_extend : 
  'a Gram.entry ->
  gram_reinit option ->
  'a Extend.extend_statment ->
  unit

module GramState : Store.S

type 'a grammar_command

type extend_rule =

type !'a grammar_extension =
  'a ->
  GramState.t ->
  extend_rule list * GramState.t

val create_grammar_command : 
  string ->
  'a grammar_extension ->
  'a grammar_command

val extend_grammar_command : 'a grammar_command -> 'a -> unit

val recover_grammar_command : 'a grammar_command -> 'a list

val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b

val to_coqloc : Ploc.t -> Loc.t

val (!@) : Ploc.t -> Loc.t

package coq