Convert 2nd part of rewriting chapter to prodn

4 files changed, 17 insertions, 17 deletions

diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 214541570c..87001251c2 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -226,10 +226,10 @@ Automatic declaration of implicit arguments
       Print Implicit nil.
 
 The computation of implicit arguments takes account of the unfolding
-of constants. For instance, the variable ``p`` below has type
+of :term:`constants <constant>`. For instance, the variable ``p`` below has type
 ``(Transitivity R)`` which is reducible to
 ``forall x,y:U, R x y -> forall z:U, R y z -> R x z``. As the variables ``x``, ``y`` and ``z``
-appear strictly in the body of the type, they are implicit.
+appear strictly in the :term:`body` of the type, they are implicit.
 
 .. coqtop:: all
 
@@ -318,7 +318,7 @@ Binding arguments to a scope
 Effects of :cmd:`Arguments` on unfolding
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-+ `simpl never` indicates that a constant should never be unfolded by :tacn:`cbn`,
++ `simpl never` indicates that a :term:`constant` should never be unfolded by :tacn:`cbn`,
   :tacn:`simpl` or :tacn:`hnf`:
 
   .. example::
@@ -330,7 +330,7 @@ Effects of :cmd:`Arguments` on unfolding
   After that command an expression like :g:`(minus (S x) y)` is left
   untouched by the tactics :tacn:`cbn` and :tacn:`simpl`.
 
-+ A constant can be marked to be unfolded only if it's applied to at least
++ A :term:`constant` can be marked to be unfolded only if it's applied to at least
   the arguments appearing before the `/` in a :cmd:`Arguments` command.
 
   .. example::
@@ -343,7 +343,7 @@ Effects of :cmd:`Arguments` on unfolding
 
   After that command the expression :g:`(f \o g)` is left untouched by
   :tacn:`simpl` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`.
-  The same mechanism can be used to make a constant volatile, i.e.
+  The same mechanism can be used to make a :term:`constant` volatile, i.e.
   always unfolded.
 
   .. example::
@@ -353,7 +353,7 @@ Effects of :cmd:`Arguments` on unfolding
         Definition volatile := fun x : nat => x.
         Arguments volatile / x.
 
-+ A constant can be marked to be unfolded only if an entire set of
++ A :term:`constant` can be marked to be unfolded only if an entire set of
   arguments evaluates to a constructor. The ``!`` symbol can be used to mark
   such arguments.
 
@@ -366,7 +366,7 @@ Effects of :cmd:`Arguments` on unfolding
   After that command, the expression :g:`(minus (S x) y)` is left untouched
   by :tacn:`simpl`, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`.
 
-+ `simpl nomatch` indicates that a constant should not be unfolded if it would expose
++ `simpl nomatch` indicates that a :term:`constant` should not be unfolded if it would expose
   a `match` construct in the head position.  This affects the :tacn:`cbn`,
   :tacn:`simpl` and :tacn:`hnf` tactics.
 
@@ -379,10 +379,10 @@ Effects of :cmd:`Arguments` on unfolding
   In this case, :g:`(minus (S (S x)) (S y))` is simplified to :g:`(minus (S x) y)`
   even if an extra simplification is possible.
 
-  In detail: the tactic :tacn:`simpl` first applies :math:`\beta`:math:`\iota`-reduction. Then, it
-  expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`-reduction.
-  But, when no :math:`\iota` rule is applied after unfolding then
-  :math:`\delta`-reductions are not applied. For instance trying to use :tacn:`simpl` on
+  In detail: the tactic :tacn:`simpl` first applies βι-reduction. Then, it
+  expands transparent :term:`constants <constant>` and tries to reduce further using βι-reduction.
+  But, when no ι rule is applied after unfolding then
+  δ-reductions are not applied. For instance trying to use :tacn:`simpl` on
   :g:`(plus n O) = n` changes nothing.
 
 
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index 4cc35794cc..fbba6c30b8 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -34,7 +34,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
    The first form of this command declares an existing :n:`@reference` as a
    canonical instance of a structure (a record).
 
-   The second form defines a new constant as if the :cmd:`Definition` command
+   The second form defines a new :term:`constant` as if the :cmd:`Definition` command
    had been used, then declares it as a canonical instance as if the first
    form had been used on the defined object.
 
@@ -113,7 +113,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
    This displays the list of global names that are components of some
    canonical structure. For each of them, the canonical structure of
-   which it is a projection is indicated. If constants are given as
+   which it is a projection is indicated. If :term:`constants <constant>` are given as
    its arguments, only the unification rules that involve or are
    synthesized from simultaneously all given constants will be shown.
 
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index 765d04ec88..76a4d4a6ff 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -238,7 +238,7 @@ Here is an example:
 
    This is triggered when setting an argument implicit in an
    expression which does not correspond to the type of an assumption
-   or to the body of a definition. Here is an example:
+   or to the :term:`body` of a definition. Here is an example:
 
    .. coqtop:: all warn
 
@@ -448,7 +448,7 @@ function.
 
    Turning this flag on (it is off by default) deactivates the use of implicit arguments.
 
-   In this case, all arguments of constants, inductive types,
+   In this case, all arguments of :term:`constants <constant>`, inductive types,
    constructors, etc, including the arguments declared as implicit, have
    to be given as if no arguments were implicit. By symmetry, this also
    affects printing.
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 1c022448b0..818d130042 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -300,7 +300,7 @@ Conventions about unused pattern-matching variables
 
 Pattern-matching variables that are not used on the right-hand side of ``=>`` are
 considered the sign of a potential error. For instance, it could
-result from an undetected mispelled constant constructor. By default,
+result from an undetected misspelled constant constructor. By default,
 a warning is issued in such situations.
 
 .. warn:: Unused variable @ident catches more than one case.
@@ -366,7 +366,7 @@ only simple patterns remain. The original nesting of the ``match`` expressions
 is recovered at printing time. An easy way to see the result
 of the expansion is to toggle off the nesting performed at printing
 (use here :flag:`Printing Matching`), then by printing the term with :cmd:`Print`
-if the term is a constant, or using the command :cmd:`Check`.
+if the term is a :term:`constant`, or using the command :cmd:`Check`.
 
 The extended ``match`` still accepts an optional *elimination predicate*
 given after the keyword ``return``. Given a pattern matching expression,