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
val get_univ : string -> gram_universe
val create_universe : string -> gram_universe
val new_entry : gram_universe -> string -> 'a Entry.t
val uprim : gram_universe
val uconstr : gram_universe
val utactic : gram_universe
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
val create_generic_entry : gram_universe -> string -> ('a, Genarg.rlevel) Genarg.abstract_argument_type -> 'a 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct