package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val add_token_obj : string -> unit
val add_notation_extra_printing_rule : string -> string -> string -> unit
val declare_scope : Vernacexpr.locality_flag -> Notation_term.scope_name -> unit
val add_delimiters : Vernacexpr.locality_flag -> Notation_term.scope_name -> string -> unit
val remove_delimiters : Vernacexpr.locality_flag -> Notation_term.scope_name -> unit
val add_notation_interpretation : Environ.env -> (Names.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) -> unit
val set_notation_for_interpretation : Environ.env -> Constrintern.internalization_env -> (Names.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) -> unit
val add_syntax_extension : Vernacexpr.locality_flag -> (Names.lstring * Vernacexpr.syntax_modifier list) -> unit
val add_syntactic_definition : Environ.env -> Names.Id.t -> (Names.Id.t list * Constrexpr.constr_expr) -> bool -> Flags.compat_version option -> unit
val pr_grammar : string -> Pp.t
val pr_custom_grammar : string -> Pp.t
val check_infix_modifiers : Vernacexpr.syntax_modifier list -> unit
val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
val declare_custom_entry : Vernacexpr.locality_flag -> string -> 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