Properly document the local and global locality attributes.

2 files changed, 79 insertions, 20 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.