package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

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

Authors

T

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

Maintainers

C

coqdev@inria.fr

Sources

coq-8.14.1.tar.gz

sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

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

Module `Metasyntax`Source

Sourceval add_token_obj : string -> unit

Adding a (constr) notation in the environment

Source

val add_infix : 
  local:bool ->
  Deprecation.t option ->
  Environ.env ->
  (Names.lstring * Vernacexpr.syntax_modifier list) ->
  Constrexpr.constr_expr ->
  Notation_term.scope_name option ->
  unit

Source

val 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

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 only the interpretation of a notation that already has pa/pp rules

Source

val add_notation_interpretation : 
  Environ.env ->
  Vernacexpr.decl_notation ->
  unit

Add a notation interpretation for supporting the "where" clause

Source

val set_notation_for_interpretation : 
  Environ.env ->
  Constrintern.internalization_env ->
  Vernacexpr.decl_notation ->
  unit

Add only the parsing/printing rule of a notation

Source

val add_syntax_extension : 
  local:bool ->
  (Names.lstring * Vernacexpr.syntax_modifier 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 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

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module MetasyntaxSource

Module `Metasyntax`Source