Module `Metasyntax`Source

Adding a (constr) notation in the environment

val 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

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.scope_class list ->
  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

Source

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

Declare the interpretation of the where-notation

Source

val 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

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_syntactic_definition : 
  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

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Metasyntax`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module MetasyntaxSource

Module `Metasyntax`Source