Interpret the Export modifier of Set and Unset as an attribute.

Unfortunately, we cannot go further and parse Export as a legacy
attribute because this syntax conflicts with the Export command.

1 files changed, 42 insertions, 34 deletions

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 48c65f631f..895886605d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -91,34 +91,30 @@ and tables:
 Flags, options and tables are identified by a series of identifiers, each with an initial
 capital letter.
 
-.. cmd::  {? {| Local | Global | Export } } Set @flag
+.. cmd::  Set @flag
    :name: Set
 
-   Sets :token:`flag` on. Scoping qualifiers are
-   described :ref:`here <set_unset_scope_qualifiers>`.
+   Sets :token:`flag` on.
 
-.. cmd:: {? {| Local | Global | Export } } Unset @flag
+.. cmd:: Unset @flag
    :name: Unset
 
-   Sets :token:`flag` off. Scoping qualifiers are
-   described :ref:`here <set_unset_scope_qualifiers>`.
+   Sets :token:`flag` off.
 
 .. cmd:: Test @flag
 
    Prints the current value of :token:`flag`.
 
 
-.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string }
+.. cmd:: Set @option {| @num | @string }
    :name: Set @option
 
-   Sets :token:`option` to the specified value.  Scoping qualifiers are
-   described :ref:`here <set_unset_scope_qualifiers>`.
+   Sets :token:`option` to the specified value.
 
-.. cmd:: {? {| Local | Global | Export } } Unset @option
+.. cmd:: Unset @option
    :name: Unset @option
 
-   Sets :token:`option` to its default value.  Scoping qualifiers are
-   described :ref:`here <set_unset_scope_qualifiers>`.
+   Sets :token:`option` to its default value.
 
 .. cmd:: Test @option
 
@@ -157,27 +153,37 @@ capital letter.
 
    A synonym for :cmd:`Print Options`.
 
-.. _set_unset_scope_qualifiers:
+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` (an alternative syntax is to use 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` (an alternative syntax is to use 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` (an alternative syntax is to use 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.
+
+Newly opened modules and sections inherit the current settings.
 
-Scope qualifiers for :cmd:`Set` and :cmd:`Unset`
-`````````````````````````````````````````````````
-
-:n:`{? {| Local | Global | Export } }`
-
-Flag and option settings can be global in scope or local to nested scopes created by
-:cmd:`Module` and :cmd:`Section` commands.  There are four alternatives:
-
-* no qualifier: the original setting is *not* restored at the end of the current module or section.
-* **Local**: the setting is applied within the current scope.  The original value of the option
-  or flag is restored at the end of the current module or section.
-* **Global**: similar to no qualifier, 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.
-* **Export**: similar to **Local**, the original value of the option or flag is restored at the
-  end of the current module or section.  In addition, if the value is set in a file, then :cmd:`Import`-ing
-  the file sets the option.
+.. note::
 
-Newly opened scopes inherit the current settings.
+   The use of the :attr:`global` attribute with the :cmd:`Set` and
+   :cmd:`Unset` commands is discouraged.  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
+   (cf. :ref:`command-line-options`).
 
 .. _requests-to-the-environment:
 
@@ -1192,9 +1198,11 @@ Controlling the locality of commands
 
 .. 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. The :cmd:`Hint` command accepts it for instance.
+   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 :cmd:`Hint`, :cmd:`Set` and :cmd:`Unset`
+   commands.
 
 .. _controlling-typing-flags: