Documenting the new only-parsing only-printing model.

1 files changed, 30 insertions, 13 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 5148fa84c9..d6db305300 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -57,15 +57,14 @@ to represent :g:`(and A B)`:
 Notations must be in double quotes, except when the
 abbreviation has the form of an ordinary applicative expression;
 see :ref:`Abbreviations`. The notation consists of *tokens* separated by
-spaces. Alphanumeric strings (such as ``A`` and ``B``) are the *parameters*
+spaces. Tokens which are identifiers (such as ``A``, ``x0'``, etc.) are the *parameters*
 of the notation. Each of them must occur at least once in the abbreviated term. The
 other elements of the string (such as ``/\``) are the *symbols*.
 
-Substrings enclosed in single quotes are treated as literals.  This is necessary
-for substrings that would otherwise be interpreted as :n:`@ident`\s.  Similarly,
-every symbol of at least 3 characters and starting with a simple quote
-must be quoted (then it starts by two single quotes). Here is an
-example.
+Identifiers enclosed in single quotes are treated as symbols and thus
+lose their role of parameters. In the same vein, every symbol of at
+least 3 characters and starting with a simple quote must be quoted
+(then it starts with two single quotes). Here is an example.
 
 .. coqtop:: in
 
@@ -82,7 +81,8 @@ associativity rules have to be given.
    The right-hand side of a notation is interpreted at the time the notation is
    given. In particular, disambiguation of constants, :ref:`implicit arguments
    <ImplicitArguments>` and other notations are resolved at the
-   time of the declaration of the notation.
+   time of the declaration of the notation. The right-hand side is
+   currently typed only at use time but this may change in the future.
 
 Precedences and associativity
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -299,12 +299,29 @@ Notations disappear when a section is closed. No typing of the denoted
 expression is performed at definition time. Type checking is done only
 at the time of use of the notation.
 
-.. note:: Sometimes, a notation is expected only for the parser. To do
-          so, the option ``only parsing`` is allowed in the list of :n:`@syntax_modifier`\s
-          in :cmd:`Notation`. Conversely, the ``only printing`` :n:`@syntax_modifier` can be
-          used to declare that a notation should only be used for printing and
-          should not declare a parsing rule. In particular, such notations do
-          not modify the parser.
+.. note::
+
+   The default for a notation is to be used both for parsing and
+   printing. It is possible to declare a notation only for parsing by
+   adding the option ``only parsing`` to the list of
+   :n:`@syntax_modifier`\s of :cmd:`Notation`. Symmetrically, the
+   ``only printing`` :n:`@syntax_modifier` can be used to declare that
+   a notation should only be used for printing.
+
+   If a notation to be used both for parsing and printing is
+   overriden, both the parsing and printing are invalided, even if the
+   overriding rule is only parsing.
+
+   If a given notation string occurs only in ``only printing`` rules,
+   the parser is not modified at all.
+
+   To a given notation string and scope can be attached at most one
+   notation with both parsing and printing or with only
+   parsing. Contrastingly, an arbitrary number of ``only printing``
+   notations differing in their right-hand sides but only a unique
+   right-hand side can be attached to a given string and
+   scope. Obviously, expressions printed by means of such extra
+   printing rules will not be reparsed to the same form.
 
 The Infix command
 ~~~~~~~~~~~~~~~~~~