package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Gram : sig ... end
module Parsable : sig ... end
module Entry : sig ... end
val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit
val parse_string : 'a Entry.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, 'a) Extend.symbol -> 'self option
val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a Extend.extend_statement -> unit
type 'a grammar_command
type extend_rule =
  1. | ExtendRule : 'a Entry.t * gram_reinit option * 'a Extend.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
val of_coqloc : Loc.t -> Ploc.t
val to_coqloc : Ploc.t -> Loc.t
val (!@) : Ploc.t -> Loc.t
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
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