diff options
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 29 | ||||
| -rw-r--r-- | doc/sphinx/language/core/modules.rst | 70 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 51 |
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 |