Module `Metasyntax`Source

Sourcetype notation_main_data

Sourcetype syntax_rules

Sourcetype notation_interpretation_decl

This data type packages all the necessary information to declare a notation interpretation, once the syntax is declared or recovered from a previous declaration.

Source

val add_notation_syntax : 
  local:bool ->
  infix:bool ->
  Deprecation.t option ->
  Vernacexpr.notation_declaration ->
  notation_interpretation_decl

Add syntax rules for a (constr) notation in the environment

Source

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

Declare the interpretation of a notation

Declaring scopes, delimiter keys and default scopes

Source

val declare_scope : 
  Vernacexpr.locality_flag ->
  Notation_term.scope_name ->
  unit

Source

val add_delimiters : 
  Vernacexpr.locality_flag ->
  Notation_term.scope_name ->
  string ->
  unit

Source

val remove_delimiters : 
  Vernacexpr.locality_flag ->
  Notation_term.scope_name ->
  unit

Source

val add_class_scope : 
  Vernacexpr.locality_flag ->
  Notation_term.scope_name ->
  Notation.add_scope_where option ->
  Notation.scope_class list ->
  unit

Scope opening

Source

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)

Source

val prepare_where_notation : 
  Vernacexpr.notation_declaration ->
  notation_interpretation_decl

Interpret the modifiers of a where-notation

Source

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

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

Add only the parsing/printing rule of a notation

Source

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 := ...")

Source

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

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

Source

val 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

Source

val pr_level : 
  Constrexpr.notation ->
  Notationextern.level ->
  Extend.constr_entry_key list ->
  Pp.t

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

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Metasyntax`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module MetasyntaxSource

Module `Metasyntax`Source