package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

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

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