package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Gram : sig ... end
val camlp5_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_control) 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
val grammar_extend : 'a Gram.entry -> gram_reinit option -> 'a Extend.extend_statment -> unit
type 'a grammar_command
type extend_rule =
  1. | ExtendRule : 'a Gram.entry * gram_reinit option * 'a Extend.extend_statment -> 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
type frozen_t
val parser_summary_tag : frozen_t Summary.Dyn.tag
type any_entry =
  1. | AnyEntry : 'a Gram.entry -> 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