package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val add_token_obj : string -> unit

Adding a (constr) notation in the environment

val add_infix : local:bool -> Deprecation.t option -> Environ.env -> (Names.lstring * Vernacexpr.syntax_modifier list) -> Constrexpr.constr_expr -> Notation_term.scope_name option -> unit
val add_notation : local:bool -> Deprecation.t option -> Environ.env -> Constrexpr.constr_expr -> (Names.lstring * Vernacexpr.syntax_modifier list) -> Notation_term.scope_name option -> unit
val add_notation_extra_printing_rule : string -> string -> string -> unit

Declaring scopes, delimiter keys and default scopes

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

Add only the interpretation of a notation that already has pa/pp rules

val add_notation_interpretation : Environ.env -> Vernacexpr.decl_notation -> unit

Add a notation interpretation for supporting the "where" clause

val set_notation_for_interpretation : Environ.env -> Constrintern.internalization_env -> Vernacexpr.decl_notation -> unit

Add only the parsing/printing rule of a notation

val add_syntax_extension : local:bool -> (Names.lstring * Vernacexpr.syntax_modifier list) -> unit

Add a syntactic definition (as in "Notation f := ...")

val add_syntactic_definition : local:bool -> Deprecation.t option -> Environ.env -> Names.Id.t -> (Names.Id.t list * Constrexpr.constr_expr) -> Vernacexpr.syntax_modifier list -> unit

Print the Camlp5 state of a grammar

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