Convert 2nd part of rewriting chapter to prodn

12 files changed, 108 insertions, 99 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 1cfd8dac50..9f097b4fe9 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1,8 +1,9 @@
 Typing rules
 ====================================
 
-The underlying formal language of Coq is a *Calculus of Inductive
-Constructions* (|Cic|) whose inference rules are presented in this
+The underlying formal language of Coq is a
+:gdef:`Calculus of Inductive Constructions` (|Cic|) whose inference rules
+are presented in this
 chapter. The history of this formalism as well as pointers to related
 work are provided in a separate chapter; see *Credits*.
 
@@ -146,7 +147,7 @@ In the global environment,
 :math:`(c:T)`, indicating that :math:`c` is of the type :math:`T`. *Definitions*
 are written as :math:`c:=t:T`, indicating that :math:`c` has the value :math:`t`
 and type :math:`T`. We shall call
-such names *constants*. For the rest of the chapter, the :math:`E;~c:T` denotes
+such names :term:`constants <constant>`. For the rest of the chapter, the :math:`E;~c:T` denotes
 the global environment :math:`E` enriched with the assumption :math:`c:T`.
 Similarly, :math:`E;~c:=t:T` denotes the global environment :math:`E` enriched with the
 definition :math:`(c:=t:T)`.
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index e742139134..61952c1570 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -196,5 +196,5 @@ Top-level definitions of co-recursive functions
 
    If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
-   In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
+   In this case, the proof should be terminated with :cmd:`Defined` in order to define a :term:`constant`
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst
index 09c619338b..06b6c61ea9 100644
--- a/doc/sphinx/language/core/conversion.rst
+++ b/doc/sphinx/language/core/conversion.rst
@@ -1,11 +1,13 @@
 .. _Conversion-rules:
 
 Conversion rules
---------------------
+----------------
 
-In |Cic|, there is an internal reduction mechanism. In particular, it
-can decide if two programs are *intentionally* equal (one says
-:term:`convertible`). Convertibility is described in this section.
+Coq has conversion rules that can be used to determine if two
+terms are equal by definition, or :term:`convertible`.
+Conversion rules consist of reduction rules and expansion rules.
+See :ref:`applyingconversionrules`,
+which describes tactics that apply these conversion rules.
 
 α-conversion
 ~~~~~~~~~~~~
@@ -14,56 +16,44 @@ Two terms are :gdef:`α-convertible <alpha-convertible>` if they are syntactical
 equal ignoring differences in the names of variables bound within the expression.
 For example `forall x, x + 0 = x` is α-convertible with `forall y, y + 0 = y`.
 
-.. _beta-reduction:
-
 β-reduction
 ~~~~~~~~~~~
 
-We want to be able to identify some terms as we can identify the
-application of a function to a given argument with its result. For
-instance the identity function over a given type :math:`T` can be written
-:math:`λx:T.~x`. In any global environment :math:`E` and local context
-:math:`Γ`, we want to identify any object :math:`a` (of type
-:math:`T`) with the application :math:`((λ x:T.~x)~a)`.  We define for
-this a *reduction* (or a *conversion*) rule we call :math:`β`:
+:gdef:`β-reduction <beta-reduction>` reduces a :gdef:`beta-redex`, which is
+a term in the form `(fun x => t) u`.  (Beta-redex
+is short for "beta-reducible expression", a term from lambda calculus.
+See `Beta reduction <https://en.wikipedia.org/wiki/Beta_normal_form#Beta_reduction>`_
+for more background.)
 
-.. math::
+Formally, in any :term:`global environment` :math:`E` and :term:`local context`
+:math:`Γ`, the beta-reduction rule is:
 
-        E[Γ] ⊢ ((λx:T.~t)~u)~\triangleright_β~\subst{t}{x}{u}
+.. inference:: Beta
+
+   --------------
+   E[Γ] ⊢ ((λx:T.~t)~u)~\triangleright_β~\subst{t}{x}{u}
 
 We say that :math:`\subst{t}{x}{u}` is the *β-contraction* of
 :math:`((λx:T.~t)~u)` and, conversely, that :math:`((λ x:T.~t)~u)` is the
 *β-expansion* of :math:`\subst{t}{x}{u}`.
 
-According to β-reduction, terms of the *Calculus of Inductive
-Constructions* enjoy some fundamental properties such as confluence,
+.. todo: :term:`Calculus of Inductive Constructions` fails to build in CI for some reason :-()
+
+Terms of the *Calculus of Inductive Constructions*
+enjoy some fundamental properties such as confluence,
 strong normalization, subject reduction. These results are
 theoretically of great importance but we will not detail them here and
 refer the interested reader to :cite:`Coq85`.
 
-
-.. _iota-reduction:
-
-ι-reduction
-~~~~~~~~~~~
-
-A specific conversion rule is associated with the inductive objects in
-the global environment. We shall give later on (see Section
-:ref:`Well-formed-inductive-definitions`) the precise rules but it
-just says that a destructor applied to an object built from a
-constructor behaves as expected. This reduction is called ι-reduction
-and is more precisely studied in :cite:`Moh93,Wer94`.
-
-
-.. _delta-reduction:
+.. _delta-reduction-sect:
 
 δ-reduction
 ~~~~~~~~~~~
 
-We may have variables defined in local contexts or constants defined
-in the global environment. It is legal to identify such a reference
-with its value, that is to expand (or unfold) it into its value. This
-reduction is called δ-reduction and shows as follows.
+:gdef:`δ-reduction <delta-reduction>` replaces variables defined in
+:term:`local contexts <local context>`
+or :term:`constants <constant>` defined in the :term:`global environment` with their values.
+:gdef:`Unfolding <unfold>` means to replace a constant by its definition. Formally, this is:
 
 .. inference:: Delta-Local
 
@@ -79,16 +69,29 @@ reduction is called δ-reduction and shows as follows.
    --------------
    E[Γ] ⊢ c~\triangleright_δ~t
 
+:term:`Delta-reduction <delta-reduction>` only unfolds :term:`constants <constant>` that are
+marked :gdef:`transparent`.  :gdef:`Opaque <opaque>` is the opposite of
+transparent; :term:`delta-reduction` doesn't unfold opaque constants.
+
+ι-reduction
+~~~~~~~~~~~
 
-.. _zeta-reduction:
+A specific conversion rule is associated with the inductive objects in
+the global environment. We shall give later on (see Section
+:ref:`Well-formed-inductive-definitions`) the precise rules but it
+just says that a destructor applied to an object built from a
+constructor behaves as expected. This reduction is called
+:gdef:`ι-reduction <iota-reduction>`
+and is more precisely studied in :cite:`Moh93,Wer94`.
 
 ζ-reduction
 ~~~~~~~~~~~
 
-Coq allows also to remove local definitions occurring in terms by
-replacing the defined variable by its value. The declaration being
-destroyed, this reduction differs from δ-reduction. It is called
-ζ-reduction and shows as follows.
+:gdef:`ζ-reduction <zeta-reduction>` removes :ref:`let-in definitions <let-in>`
+in terms by
+replacing the defined variable by its value. One way this reduction differs from
+δ-reduction is that the declaration is removed from the term entirely.
+Formally, this is:
 
 .. inference:: Zeta
 
@@ -99,12 +102,12 @@ destroyed, this reduction differs from δ-reduction. It is called
    E[Γ] ⊢ \letin{x}{u:U}{t}~\triangleright_ζ~\subst{t}{x}{u}
 
 
-.. _eta-expansion:
+.. _eta-expansion-sect:
 
 η-expansion
 ~~~~~~~~~~~
 
-Another important concept is η-expansion. It is legal to identify any
+Another important concept is :gdef:`η-expansion <eta-expansion>`. It is legal to identify any
 term :math:`t` of functional type :math:`∀ x:T,~U` with its so-called η-expansion
 
 .. math::
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 7196c082ed..fcf61a5bf4 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -31,43 +31,48 @@ for :n:`let @ident := fun {+ @binder} => @term__1 in @term__2`.
    single: ... <: ...
    single: ... <<: ...
 
+.. _type-cast:
+
 Type cast
 ---------
 
 .. insertprodn term_cast term_cast
 
 .. prodn::
-   term_cast ::= @term10 <: @type
+   term_cast ::= @term10 : @type
+   | @term10 <: @type
    | @term10 <<: @type
-   | @term10 : @type
    | @term10 :>
 
 The expression :n:`@term10 : @type` is a type cast expression. It enforces
 the type of :n:`@term10` to be :n:`@type`.
 
-:n:`@term10 <: @type` locally sets up the virtual machine for checking that
-:n:`@term10` has type :n:`@type`.
+:n:`@term10 <: @type` specifies that the virtual machine will be used
+to type check that :n:`@term10` has type :n:`@type` (see :tacn:`vm_compute`).
+
+:n:`@term10 <<: @type` specifies that compilation to OCaml will be used
+to type check that :n:`@term10` has type :n:`@type` (see :tacn:`native_compute`).
 
-:n:`@term10 <<: @type` uses native compilation for checking that :n:`@term10`
-has type :n:`@type`.
+:n:`@term10 :>` casts to the support type in Program mode.
+See :ref:`syntactic_control`.
 
 .. _gallina-definitions:
 
 Top-level definitions
 ---------------------
 
-Definitions extend the global environment with associations of names to terms.
+Definitions extend the global environment by associating names to terms.
 A definition can be seen as a way to give a meaning to a name or as a
 way to abbreviate a term. In any case, the name can later be replaced at
 any time by its definition.
 
 The operation of unfolding a name into its definition is called
-:math:`\delta`-conversion (see Section :ref:`delta-reduction`). A
-definition is accepted by the system if and only if the defined term is
+:term:`delta-reduction`.
+A definition is accepted by the system if and only if the defined term is
 well-typed in the current context of the definition and if the name is
 not already used. The name defined by the definition is called a
-*constant* and the term it refers to is its *body*. A definition has a
-type which is the type of its body.
+:gdef:`constant` and the term it refers to is its :gdef:`body`. A definition has
+a type, which is the type of its :term:`body`.
 
 A formal presentation of constants and environments is given in
 Section :ref:`typing-rules`.
@@ -96,7 +101,7 @@ Section :ref:`typing-rules`.
 
    If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
-   In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
+   In this case, the proof should be terminated with :cmd:`Defined` in order to define a :term:`constant`
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
 
    The form :n:`Definition @ident : @type := @term` checks that the type of :n:`@term`
@@ -151,7 +156,7 @@ The basic assertion command is:
    over a mutually inductive assumption, or that assert mutually dependent
    statements in some mutual co-inductive type. It is equivalent to
    :cmd:`Fixpoint` or :cmd:`CoFixpoint` but using tactics to build the proof of
-   the statements (or the body of the specification, depending on the point of
+   the statements (or the :term:`body` of the specification, depending on the point of
    view). The inductive or co-inductive types on which the induction or
    coinduction has to be done is assumed to be non ambiguous and is guessed by
    the system.
@@ -202,10 +207,10 @@ the proof and adds it to the global environment.
       statements still to be proved. Nonetheless, this practice is discouraged
       and may stop working in future versions.
 
-   #. Proofs ended by :cmd:`Qed` are declared opaque. Their content cannot be
-      unfolded (see :ref:`performingcomputations`), thus
-      realizing some form of *proof-irrelevance*. To be able to unfold a
-      proof, the proof should be ended by :cmd:`Defined`.
+   #. Proofs ended by :cmd:`Qed` are declared :term:`opaque`. Their content cannot be
+      unfolded (see :ref:`applyingconversionrules`), thus
+      realizing some form of *proof-irrelevance*.
+      Proofs that end with :cmd:`Defined` can be unfolded.
 
    #. :cmd:`Proof` is recommended but can currently be omitted. On the opposite
       side, :cmd:`Qed` (or :cmd:`Defined`) is mandatory to validate a proof.
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 4e892f709d..971a856899 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -25,7 +25,7 @@ Inductive types
    respectively correspond to elimination principles on :g:`Type`, :g:`Prop`,
    :g:`Set` and :g:`SProp`.  The type of the destructors
    expresses structural induction/recursion principles over objects of
-   type :n:`@ident`.  The constant :n:`@ident`\ ``_ind`` is always
+   type :n:`@ident`.  The :term:`constant` :n:`@ident`\ ``_ind`` is always
    generated, whereas :n:`@ident`\ ``_rec`` and :n:`@ident`\ ``_rect``
    may be impossible to derive (for example, when :n:`@ident` is a
    proposition).
@@ -415,7 +415,7 @@ constructions.
 
    If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
-   In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
+   In this case, the proof should be terminated with :cmd:`Defined` in order to define a :term:`constant`
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
 
    This command accepts the :attr:`using` attribute.
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 2e678c49d8..c42d444089 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -17,7 +17,7 @@ and :math:`id` an identifier, then :math:`p′.id` is an access path.
 
 
 **Structure element.** A structure element is denoted by :math:`e` and
-is either a definition of a constant, an assumption, a definition of
+is either a definition of a :term:`constant`, an assumption, a definition of
 an inductive, a definition of a module, an alias of a module or a module
 type abbreviation.
 
@@ -134,7 +134,7 @@ is also used to terminate :ref:`Sections<section-mechanism>`.
 :n:`End @ident` closes the interactive module or module type :token:`ident`.
 If the module type was given, the command verifies that the content of the module
 matches the module type.  If the module is not a
-functor, its components (constants, inductive types, submodules etc.)
+functor, its components (:term:`constants <constant>`, inductive types, submodules etc.)
 are now available through the dot notation.
 
 .. exn:: No such label @ident.
@@ -170,7 +170,7 @@ are now available through the dot notation.
      hints and the like valid for :n:`@ident__1` are the ones defined in :n:`@module_type`
      rather then those defined in :n:`@ident__2` (or the module body).
   #. Within an interactive module type definition, the :cmd:`Parameter` command declares a
-     constant instead of definining a new axiom (which it does when not in a module type definition).
+     :term:`constant` instead of definining a new axiom (which it does when not in a module type definition).
   #. Assumptions such as :cmd:`Axiom` that include the :n:`Inline` clause will be automatically
      expanded when the functor is applied, except when the function application is prefixed by ``!``.
 
@@ -250,14 +250,14 @@ are now available through the dot notation.
    make only those names available with short names, not other names
    defined in the module nor will it activate other features.
 
-   The names to import may be constants, inductive types and
+   The names to import may be :term:`constants <constant>`, inductive types and
    constructors, and notation aliases (for instance, Ltac definitions
    cannot be selectively imported). If they are from an inner module
    to the one being imported, they must be prefixed by the inner path.
 
    The name of an inductive type may also be followed by ``(..)`` to
    import it, its constructors and its eliminators if they exist. For
-   this purpose "eliminator" means a constant in the same module whose
+   this purpose "eliminator" means a :term:`constant` in the same module whose
    name is the inductive type's name suffixed by one of ``_sind``,
    ``_ind``, ``_rec`` or ``_rect``.
 
@@ -332,7 +332,7 @@ Examples
        Defined.
        End M.
 
-Inside a module one can define constants, prove theorems and do anything
+Inside a module one can define :term:`constants <constant>`, prove theorems and do anything
 else that can be done in the toplevel. Components of a closed
 module can be accessed using the dot notation:
 
@@ -455,9 +455,9 @@ Typing Modules
 
 In order to introduce the typing system we first slightly extend the syntactic
 class of terms and environments given in section :ref:`The-terms`. The
-environments, apart from definitions of constants and inductive types now also
-hold any other structure elements. Terms, apart from variables, constants and
-complex terms, include also access paths.
+environments, apart from definitions of :term:`constants <constant>` and inductive types now also
+hold any other structure elements. Terms, apart from variables, :term:`constants <constant>` and
+complex terms, also include access paths.
 
 We also need additional typing judgments:
 
diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index 6671c67fb2..871bc0770c 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -207,7 +207,7 @@ other arguments are the parameters of the inductive type.
   There may be three reasons:
 
   #. The name :token:`ident` already exists in the global environment (see :cmd:`Axiom`).
-  #. The body of :token:`ident` uses an incorrect elimination for
+  #. The :term:`body` of :token:`ident` uses an incorrect elimination for
      :token:`ident` (see :cmd:`Fixpoint` and :ref:`Destructors`).
   #. The type of the projections :token:`ident` depends on previous
      projections which themselves could not be defined.
@@ -278,7 +278,7 @@ There are currently two ways to introduce primitive records types:
    `r` ``= Build_``\ `R` ``(``\ `r`\ ``.(``\ |p_1|\ ``) …`` `r`\ ``.(``\ |p_n|\ ``))``.
    Eta-conversion allows to define dependent elimination for these types as well.
 #. Through the ``Inductive`` and ``CoInductive`` commands, when
-   the body of the definition is a record declaration of the form
+   the :term:`body` of the definition is a record declaration of the form
    ``Build_``\ `R` ``{`` |p_1| ``:`` |t_1|\ ``; … ;`` |p_n| ``:`` |t_n| ``}``.
    In this case the types can be recursive and eta-conversion is disallowed. These kind of record types
    differ from their traditional versions in the sense that dependent
@@ -290,11 +290,11 @@ Reduction
 
 The basic reduction rule of a primitive projection is
 |p_i| ``(Build_``\ `R` |t_1| … |t_n|\ ``)`` :math:`{\rightarrow_{\iota}}` |t_i|.
-However, to take the :math:`{\delta}` flag into
+However, to take the δ flag into
 account, projections can be in two states: folded or unfolded. An
 unfolded primitive projection application obeys the rule above, while
 the folded version delta-reduces to the unfolded version. This allows to
-precisely mimic the usual unfolding rules of constants. Projections
+precisely mimic the usual unfolding rules of :term:`constants <constant>`. Projections
 obey the usual ``simpl`` flags of the ``Arguments`` command in particular.
 There is currently no way to input unfolded primitive projections at the
 user-level, and there is no way to display unfolded projections differently
@@ -305,8 +305,8 @@ Compatibility Projections and :g:`match`
 ++++++++++++++++++++++++++++++++++++++++
 
 To ease compatibility with ordinary record types, each primitive
-projection is also defined as a ordinary constant taking parameters and
-an object of the record type as arguments, and whose body is an
+projection is also defined as an ordinary :term:`constant` taking parameters and
+an object of the record type as arguments, and whose :term:`body` is an
 application of the unfolded primitive projection of the same name. These
 constants are used when elaborating partial applications of the
 projection. One can distinguish them from applications of the primitive
diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
index c16152ff4f..4c41ce8a89 100644
--- a/doc/sphinx/language/core/sections.rst
+++ b/doc/sphinx/language/core/sections.rst
@@ -55,7 +55,7 @@ usable outside the section as shown in this :ref:`example <section_local_declara
    :name: Let; Let Fixpoint; Let CoFixpoint
 
    These are similar to :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, except that
-   the declared constant is local to the current section.
+   the declared :term:`constant` is local to the current section.
    When the section is closed, all persistent
    definitions and theorems within it that depend on the constant
    will be wrapped with a :n:`@term_let` with the same declaration.
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,