Documentation of the rules for printing notations depending on scopes.

Mostly courtesy of Jason Gross.

1 files changed, 40 insertions, 0 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 1c53f5981d..66fa3af052 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1040,6 +1040,8 @@ interpreted in the scope stack extended with the scope bound tokey.
    To remove a delimiting key of a scope, use the command
    :n:`Undelimit Scope @scope`
 
+.. _ArgumentScopes:
+
 Binding arguments of a constant to an interpretation scope
 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 
@@ -1307,6 +1309,44 @@ Displaying information about scopes
       It also displays the delimiting key if any and the class to which the
       scope is bound, if any.
 
+Impact of scopes on printing
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+When several notations are available for printing the same expression,
+Coq will use the following rules for printing priorities:
+
+- If two notations are available in different scopes which are open,
+  the notation in the more recently opened scope takes precedence.
+
+- If two notations are available in the same scope, the more recently
+  defined (or imported) notation takes precedence.
+
+- Abbreviations and lonely notations, both of which have no scope,
+  take precedence over a notation in an open scope if and only if the
+  abbreviation or lonely notation was defined (or imported) more
+  recently than when the corresponding scope was open. They take
+  precedence over any notation not in an open scope, whether this scope
+  has a delimiter or not.
+
+- A scope is *active* for printing a term either because it was opened
+  with :cmd:`Open Scope`, or the term is the immediate argument of a
+  constant which temporarily opens a scope for this argument (see
+  :ref:`Arguments <ArgumentScopes>`) in which case this temporary
+  scope is the most recent open one.
+
+- In case no abbreviation, nor lonely notation, nor notation in an
+  explicitly open scope, nor notation in a temporarily open scope of
+  arguments, has been found, notations in those closed scopes which
+  have a delimiter are considered. A notation is chosen and the
+  corresponding delimiter is inserted, making the corresponding scope
+  the most recent explicitly open scope for all subterms of the
+  current term.
+
+- A scope can be closed by using :cmd:`Close Scope` and its delimiter
+  removed by using :cmd:`Undelimit Scope`. To remove automatic
+  temporary opening of scopes for arguments of a constant, use
+  :ref:`Arguments <ArgumentScopes>`.
+
 .. _Abbreviations:
 
 Abbreviations