package coq

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

Module MetasyntaxSource

Adding a (constr) notation in the environment

Sourceval 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
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 a notation interpretation associated to a "where" clause (already has pa/pp rules)

Sourcetype where_decl_notation
Sourceval prepare_where_notation : Vernacexpr.decl_notation -> where_decl_notation

Interpret the modifiers of a where-notation

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

Declare the interpretation of the where-notation

Sourceval 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

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

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

Sourceval 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

Sourceval pr_grammar : string -> Pp.t
Sourceval pr_custom_grammar : string -> Pp.t
Sourceval with_syntax_protection : ('a -> 'b) -> 'a -> 'b
Sourceval declare_custom_entry : Vernacexpr.locality_flag -> string -> unit

Declare given string as a custom grammar entry

Sourceval 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