package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Adding a (constr) notation in the environment

val add_notation : local:bool -> infix:bool -> Deprecation.t option -> Environ.env -> Constrexpr.constr_expr -> (Names.lstring * Vernacexpr.syntax_modifier CAst.t list) -> Notation_term.scope_name option -> 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

Scope opening

val open_close_scope : Vernacexpr.locality_flag -> to_open:bool -> Notation_term.scope_name -> unit

Add a notation interpretation associated to a "where" clause (already has pa/pp rules)

type where_decl_notation
val prepare_where_notation : Vernacexpr.decl_notation -> where_decl_notation

Interpret the modifiers of a where-notation

val add_notation_interpretation : local:bool -> Environ.env -> where_decl_notation -> unit

Declare the interpretation of the where-notation

val set_notation_for_interpretation : Environ.env -> Constrintern.internalization_env -> where_decl_notation -> unit

Set the interpretation of the where-notation for interpreting a mutual block

Add only the parsing/printing rule of a notation

val add_reserved_notation : local:bool -> infix:bool -> (Names.lstring * Vernacexpr.syntax_modifier CAst.t list) -> unit

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

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

Print the Camlp5 state of a grammar

val pr_grammar : string list -> Pp.t
val pr_custom_grammar : string -> Pp.t
val pr_keywords : unit -> Pp.t
val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
val declare_notation_toggle : Vernacexpr.locality_flag -> on:bool -> all:bool -> Notation.notation_query_pattern -> unit
val declare_custom_entry : Vernacexpr.locality_flag -> string -> unit

Declare given string as a custom grammar entry

val check_custom_entry : string -> unit

Check that the given string is a valid custom entry that has been declared

Pretty print level information of a notation and all of its arguments

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