From e02120ed6580733db2276f0c11b4f432ea670ee3 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 12 Sep 2020 20:54:22 -0700 Subject: Convert rewriting and proof-mode chapters to prodn --- doc/sphinx/language/core/basic.rst | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'doc/sphinx/language/core/basic.rst') 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 `, + contexts (:ref:`proof mode `, :ref:`custom entries `...). .. warning:: @@ -332,9 +332,9 @@ rest of the Coq manual: :term:`terms ` 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. -- cgit v1.2.3