package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module MetasyntaxSource

Sourceval add_token_obj : string -> unit

Adding a (constr) notation in the environment

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

Declaring scopes, delimiter keys and default scopes

Sourceval add_delimiters : Vernacexpr.locality_flag -> Notation_term.scope_name -> string -> unit
Sourceval remove_delimiters : Vernacexpr.locality_flag -> Notation_term.scope_name -> unit

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

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

Add a notation interpretation for supporting the "where" clause

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

Add only the parsing/printing rule of a notation

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

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

Sourceval 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

Sourceval pr_grammar : string -> Pp.t
Sourceval pr_custom_grammar : string -> Pp.t
Sourceval check_infix_modifiers : Vernacexpr.syntax_modifier list -> unit
Sourceval with_syntax_protection : ('a -> 'b) -> 'a -> 'b
Sourceval 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