package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type te = Tok.t
type !'a pattern = 'a Tok.p
module Parsable : sig ... end
val tokens : string -> (string option * int) list
module Entry : sig ... end
module Symbol : sig ... end
module Rule : sig ... end
module Rules : sig ... end
module Production : sig ... end
type 'a single_extend_statement = string option * Gramlib.Gramext.g_assoc option * 'a Production.t list
type !'a extend_statement = {
  1. pos : Gramlib.Gramext.position option;
  2. data : 'a single_extend_statement list;
}
val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, Gramlib__Grammar.norec, 'c) Symbol.t option
val mk_rule : 'a pattern list -> string Rules.t
val level_of_nonterm : ('a, Gramlib__Grammar.norec, 'c) Symbol.t -> string option
module Lookahead : sig ... end
val parse_string : 'a Entry.t -> ?loc:Loc.t -> string -> 'a
val eoi_entry : 'a Entry.t -> 'a Entry.t
val map_entry : ('a -> 'b) -> 'a Entry.t -> 'b Entry.t
type gram_universe
  • deprecated Deprecated in 8.13
val get_univ : string -> gram_universe
  • deprecated Deprecated in 8.13
val create_universe : string -> gram_universe
  • deprecated Deprecated in 8.13
val new_entry : gram_universe -> string -> 'a Entry.t
  • deprecated Deprecated in 8.13
val uprim : gram_universe
  • deprecated Deprecated in 8.13
val uconstr : gram_universe
  • deprecated Deprecated in 8.13
val utactic : gram_universe
  • deprecated Deprecated in 8.13
val create_generic_entry : gram_universe -> string -> ('a, Genarg.rlevel) Genarg.abstract_argument_type -> 'a Entry.t
  • deprecated Deprecated in 8.13. Use create_generic_entry2 instead.
val create_generic_entry2 : string -> ('a, Genarg.rlevel) Genarg.abstract_argument_type -> 'a Entry.t
val register_grammar : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw Entry.t -> unit
val genarg_grammar : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw Entry.t
module Prim : sig ... end
module Constr : sig ... end
module Module : sig ... end
val epsilon_value : ('a -> 'self) -> ('self, 'b, 'a) Symbol.t -> 'self option
val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit
type 'a grammar_command
type extend_rule =
  1. | ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
  2. | ExtendRuleReinit : 'a0 Entry.t * gram_reinit * 'a0 extend_statement -> 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
type ('a, 'b) entry_command
type (!'a, 'b) entry_extension = 'a -> GramState.t -> string list * GramState.t
val create_entry_command : string -> ('a, 'b) entry_extension -> ('a, 'b) entry_command
val extend_entry_command : ('a, 'b) entry_command -> 'a -> 'b Entry.t list
val find_custom_entry : ('a, 'b) entry_command -> string -> 'b Entry.t
val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
type frozen_t
val parser_summary_tag : frozen_t Summary.Dyn.tag
type any_entry =
  1. | AnyEntry : 'a Entry.t -> any_entry
val register_grammars_by_name : string -> any_entry list -> unit
val find_grammars_by_name : string -> any_entry list
val freeze : marshallable:bool -> frozen_t
val unfreeze : frozen_t -> unit