diff options
Diffstat (limited to 'doc/sphinx/language/core/basic.rst')
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 37 |
1 files changed, 12 insertions, 25 deletions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 2b262b89c0..2b50d4c420 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -64,7 +64,7 @@ appending the level to the nonterminal name (as in :n:`@term100` or populated by notations or plugins. Furthermore, some parsing rules are only activated in certain - contexts (:ref:`interactive proof mode <proofhandling>`, + contexts (:ref:`proof mode <proofhandling>`, :ref:`custom entries <custom-entries>`...). .. warning:: @@ -332,9 +332,9 @@ rest of the Coq manual: :term:`terms <term>` and :term:`types tactic - Tactics specify how to transform the current proof state as a + A :production:`tactic` specifies how to transform the current proof state as a step in creating a proof. They are syntactically valid only when - Coq is in proof mode, such as after a :cmd:`Theorem` command + Coq is in :term:`proof mode`, such as after a :cmd:`Theorem` command and before any subsequent proof-terminating command such as :cmd:`Qed`. See :ref:`proofhandling` for more on proof mode. @@ -450,7 +450,6 @@ they appear after a boldface label. They are listed in the :ref:`options_index`. .. cmd:: Set @setting_name {? {| @integer | @string } } - :name: Set If :n:`@setting_name` is a flag, no value may be provided; the flag is set to on. @@ -471,7 +470,6 @@ they appear after a boldface label. They are listed in the Coq versions. .. cmd:: Unset @setting_name - :name: Unset If :n:`@setting_name` is a flag, it is set to off. If :n:`@setting_name` is an option, it is set to its default value. @@ -525,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`). |