package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

doc/coq-core.vernac/Metasyntax/index.html

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

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

Scope opening

Sourceval 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)

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 list -> Pp.t
Sourceval pr_custom_grammar : string -> Pp.t
Sourceval pr_keywords : unit -> Pp.t
Sourceval with_syntax_protection : ('a -> 'b) -> 'a -> 'b
Sourceval declare_notation_toggle : Vernacexpr.locality_flag -> on:bool -> all:bool -> Notation.notation_query_pattern -> unit
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