diff options
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6e6d66447..531295b63 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -10,12 +10,12 @@ parses and prints objects, i.e. the translations between the concrete and internal representations of terms and commands. The main commands to provide custom symbolic notations for terms are -``Notation`` and ``Infix``. They are described in section 12.1. There is also a +``Notation`` and ``Infix``. They are described in section :ref:`Notations`. There is also a variant of ``Notation`` which does not modify the parser. This provides with a form of abbreviation and it is described in Section :ref:`Abbreviations`. It is sometimes expected that the same symbolic notation has different meanings in different contexts. To achieve this form of overloading, |Coq| offers a notion -of interpretation scope. This is described in Section :ref:`scopes`. +of interpretation scope. This is described in Section :ref:`Scopes`. The main command to provide custom notations for tactics is ``Tactic Notation``. It is described in Section :ref:`TacticNotation`. @@ -24,6 +24,8 @@ It is described in Section :ref:`TacticNotation`. Set Printing Depth 50. +.. _Notations: + Notations --------- @@ -68,7 +70,7 @@ have to be given. .. note:: The right-hand side of a notation is interpreted at the time the notation is - given. In particular, disambiguiation of constants, implicit arguments (see + given. In particular, disambiguation of constants, implicit arguments (see Section :ref:`ImplicitArguments`), coercions (see Section :ref:`Coercions`), etc. are resolved at the time of the declaration of the notation. @@ -689,8 +691,7 @@ side. E.g.: Summary ~~~~~~~ -Syntax of notations -~~~~~~~~~~~~~~~~~~~ +**Syntax of notations** The different syntactic variants of the command Notation are given on the following figure. The optional :token:`scope` is described in the Section 12.2. @@ -743,8 +744,7 @@ following figure. The optional :token:`scope` is described in the Section 12.2. given to some notation, say ``"{ y } & { z }"`` in fact applies to the underlying ``"{ x }"``\-free rule which is ``"y & z"``). -Persistence of notations -~~~~~~~~~~~~~~~~~~~~~~~~ +**Persistence of notations** Notations do not survive the end of sections. @@ -753,6 +753,8 @@ Notations do not survive the end of sections. Notations survive modules unless the command ``Local Notation`` is used instead of ``Notation``. +.. _Scopes: + Interpretation scopes ---------------------- @@ -1125,6 +1127,8 @@ Displaying informations about scopes class of all the existing interpretation scopes. It also displays the lonely notations. +.. _Abbreviations: + Abbreviations -------------- @@ -1187,6 +1191,8 @@ Abbreviations denoted expression is performed at definition time. Type-checking is done only at the time of use of the abbreviation. +.. _TacticNotation: + Tactic Notations ----------------- |