diff options
| author | Jim Fehrle | 2020-09-12 20:54:22 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-12-30 11:48:37 -0800 |
| commit | e02120ed6580733db2276f0c11b4f432ea670ee3 (patch) | |
| tree | 19c809eeea61fe131e4b4b15bc0bc72c617cce53 /doc/sphinx/language/core/basic.rst | |
| parent | 532cbed036c48ed2c77528b79fc947c4bc7e1c10 (diff) | |
Convert rewriting and proof-mode chapters to prodn
Diffstat (limited to 'doc/sphinx/language/core/basic.rst')
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 2b262b89c0..0a61c4ce22 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. |