Properly document the local and global locality attributes.

3 files changed, 79 insertions, 71 deletions

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 0a61c4ce22..2b50d4c420 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -523,31 +523,20 @@ they appear after a boldface label.  They are listed in the
 Locality attributes supported by :cmd:`Set` and :cmd:`Unset`
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`,
-:attr:`global` and :attr:`export` locality attributes:
-
-* no attribute: the original setting is *not* restored at the end of
-  the current module or section.
-* :attr:`local` (or alternatively, the ``Local`` prefix): the setting
-  is applied within the current module or section.  The original value
-  of the setting is restored at the end of the current module or
-  section.
-* :attr:`export` (or alternatively, the ``Export`` prefix): similar to
-  :attr:`local`, the original value of the setting is restored at the
-  end of the current module or section.  In addition, if the value is
-  set in a module, then :cmd:`Import`\-ing the module sets the option
-  or flag.
-* :attr:`global` (or alternatively, the ``Global`` prefix): the
-  original setting is *not* restored at the end of the current module
-  or section.  In addition, if the value is set in a file, then
-  :cmd:`Require`\-ing the file sets the option.
+The :cmd:`Set` and :cmd:`Unset` commands support the mutually
+exclusive :attr:`local`, :attr:`export` and :attr:`global` locality
+attributes (or the ``Local``, ``Export`` or ``Global`` prefixes).
+
+If no attribute is specified, the original value of the flag or option
+is restored at the end of the current module but it is *not* restored
+at the end of the current section.
 
 Newly opened modules and sections inherit the current settings.
 
 .. note::
 
-   We discourage using the :attr:`global` attribute with the :cmd:`Set` and
-   :cmd:`Unset` commands.  If your goal is to define
+   We discourage using the :attr:`global` locality attribute with the
+   :cmd:`Set` and :cmd:`Unset` commands.  If your goal is to define
    project-wide settings, you should rather use the command-line
    arguments ``-set`` and ``-unset`` for setting flags and options
    (see :ref:`command-line-options`).
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 4ea9606c18..2e678c49d8 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -1010,3 +1010,73 @@ subdirectories of path). See the command :cmd:`Declare ML Module` in
 
 See :ref:`command-line-options` for a more general view over the Coq command
 line options.
+
+.. _controlling-locality-of-commands:
+
+Controlling the scope of commands with locality attributes
+----------------------------------------------------------
+
+Many commands have effects that apply only within a specific scope,
+typically the section or the module in which the command was
+called. Locality :term:`attributes <attribute>` can alter the scope of
+the effect. Below, we give the semantics of each locality attribute
+while noting a few exceptional commands for which :attr:`local` and
+:attr:`global` attributes are interpreted differently.
+
+.. attr:: local
+
+   The :attr:`local` attribute limits the effect of the command to the
+   current scope (section or module).
+
+   The ``Local`` prefix is an alternative syntax for the :attr:`local`
+   attribute (see :n:`@legacy_attr`).
+
+   .. note::
+
+      - For some commands, this is the only locality supported within
+        sections (e.g., for :cmd:`Notation`, :cmd:`Ltac` and
+        :ref:`Hint <creating_hints>` commands).
+
+      - For some commands, this is the default locality within
+        sections even though other locality attributes are supported
+        as well (e.g., for the :cmd:`Arguments` command).
+
+   .. warning::
+
+      **Exception:** when :attr:`local` is applied to
+      :cmd:`Definition`, :cmd:`Theorem` or their variants, its
+      semantics are different: it makes the defined objects available
+      only through their fully-qualified names rather than their
+      unqualified names after an :cmd:`Import`.
+
+.. attr:: export
+
+   The :attr:`export` attribute makes the effect of the command
+   persist when the section is closed and applies the effect when the
+   module containing the command is imported.
+
+   Commands supporting this attribute include :cmd:`Set`, :cmd:`Unset`
+   and the :ref:`Hint <creating_hints>` commands, although the latter
+   don't support it within sections.
+
+.. attr:: global
+
+   The :attr:`global` attribute makes the effect of the command
+   persist even when the current section or module is closed.  Loading
+   the file containing the command (possibly transitively) applies the
+   effect of the command.
+
+   The ``Global`` prefix is an alternative syntax for the
+   :attr:`global` attribute (see :n:`@legacy_attr`).
+
+   .. warning::
+
+      **Exception:** for a few commands (like :cmd:`Notation` and
+      :cmd:`Ltac`), this attribute behaves like :attr:`export`.
+
+   .. warning::
+
+      We strongly discourage using the :attr:`global` locality
+      attribute because the transitive nature of file loading gives
+      the user little control. We recommend using the :attr:`export`
+      locality attribute where it is supported.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 8d1817b61f..8db16fff69 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1058,57 +1058,6 @@ described first.
    .. seealso:: :ref:`performingcomputations`
 
 
-.. _controlling-locality-of-commands:
-
-Controlling the locality of commands
------------------------------------------
-
-.. attr:: global
-          local
-
-   Some commands support a :attr:`local` or :attr:`global` attribute
-   to control the scope of their effect.  There is also a legacy (and
-   much more commonly used) syntax using the ``Local`` or ``Global``
-   prefixes (see :n:`@legacy_attr`).  There are four kinds of
-   commands:
-
-   + Commands whose default is to extend their effect both outside the
-     section and the module or library file they occur in.  For these
-     commands, the :attr:`local` attribute limits the effect of the command to the
-     current section or module it occurs in.  As an example, the :cmd:`Coercion`
-     and :cmd:`Strategy` commands belong to this category.
-   + Commands whose default behavior is to stop their effect at the end
-     of the section they occur in but to extend their effect outside the module or
-     library file they occur in. For these commands, the :attr:`local` attribute limits the
-     effect of the command to the current module if the command does not occur in a
-     section and the :attr:`global` attribute extends the effect outside the current
-     sections and current module if the command occurs in a section. As an example,
-     the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong
-     to this category. Notice that a subclass of these commands do not support
-     extension of their scope outside sections at all and the :attr:`global` attribute is not
-     applicable to them.
-   + Commands whose default behavior is to stop their effect at the end
-     of the section or module they occur in.  For these commands, the :attr:`global`
-     attribute extends their effect outside the sections and modules they
-     occur in.  The :cmd:`Transparent` and :cmd:`Opaque` commands
-     belong to this category.
-   + Commands whose default behavior is to extend their effect outside
-     sections but not outside modules when they occur in a section and to
-     extend their effect outside the module or library file they occur in
-     when no section contains them. For these commands, the :attr:`local` attribute
-     limits the effect to the current section or module while the :attr:`global`
-     attribute extends the effect outside the module even when the command
-     occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
-     category.
-
-.. attr:: export
-
-   Some commands support an :attr:`export` attribute.  The effect of
-   the attribute is to make the effect of the command available when
-   the module containing it is imported.  It is supported in
-   particular by the :ref:`Hint <creating_hints>`, :cmd:`Set` and :cmd:`Unset`
-   commands.
-
 .. _controlling-typing-flags:
 
 Controlling Typing Flags