Convert 2nd part of rewriting chapter to prodn

author: Jim Fehrle 2020-09-12 20:54:22 -0700
committer: Jim Fehrle 2021-03-08 11:48:20 -0800
commit: 0d33024ff79c38d52fde49e23d0e45d9c22eefbe (patch)
tree: 864068cd317abebcbc0a3466a1365258729fbc40 /doc/sphinx/addendum
parent: fb0666d50e1fe95ad2325f4ef2cc9fdd2666ac8a (diff)
10 files changed, 45 insertions, 45 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 8e72bb4ffd..3c7449ee69 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -29,7 +29,7 @@ Generating ML Code
 .. note::
 
   In the following, a qualified identifier :token:`qualid`
-  can be used to refer to any kind of Coq global "object" : constant,
+  can be used to refer to any kind of Coq global "object" : :term:`constant`,
   inductive type, inductive constructor or module name.
 
 The next two commands are meant to be used for rapid preview of
@@ -128,7 +128,7 @@ wants to generate an OCaml program. The optimizations can be split in two
 groups: the type-preserving ones (essentially constant inlining and
 reductions) and the non type-preserving ones (some function
 abstractions of dummy types are removed when it is deemed safe in order
-to have more elegant types). Therefore some constants may not appear in the
+to have more elegant types). Therefore some :term:`constants <constant>` may not appear in the
 resulting monolithic OCaml program. In the case of modular extraction,
 even if some inlining is done, the inlined constants are nevertheless
 printed, to ensure session-independent programs.
@@ -166,15 +166,15 @@ and commands:
 
 .. flag:: Extraction AutoInline
 
-   Default is on. The extraction mechanism inlines the bodies of
-   some defined constants, according to some heuristics
+   Default is on. The extraction mechanism inlines the :term:`bodies <body>` of
+   some defined :term:`constants <constant>`, according to some heuristics
    like size of bodies, uselessness of some arguments, etc.
    Those heuristics are not always perfect; if you want to disable
    this feature, turn this flag off.
 
 .. cmd:: Extraction Inline {+ @qualid }
 
-   In addition to the automatic inline feature, the constants
+   In addition to the automatic inline feature, the :term:`constants <constant>`
    mentioned by this command will always be inlined during extraction.
 
 .. cmd:: Extraction NoInline {+ @qualid }
@@ -194,24 +194,24 @@ and commands:
 
 **Inlining and printing of a constant declaration:**
 
-The user can explicitly ask for a constant to be extracted by two means:
+The user can explicitly ask for a :term:`constant` to be extracted by two means:
 
   * by mentioning it on the extraction command line
 
-  * by extracting the whole Coq module of this constant.
+  * by extracting the whole Coq module of this :term:`constant`.
 
-In both cases, the declaration of this constant will be present in the
-produced file. But this same constant may or may not be inlined in
+In both cases, the declaration of this :term:`constant` will be present in the
+produced file. But this same :term:`constant` may or may not be inlined in
 the following terms, depending on the automatic/custom inlining mechanism.  
 
-For the constants non-explicitly required but needed for dependency
+For the :term:`constants <constant>` non-explicitly required but needed for dependency
 reasons, there are two cases: 
 
   * If an inlining decision is taken, whether automatically or not,
-    all occurrences of this constant are replaced by its extracted body,
-    and this constant is not declared in the generated file.
+    all occurrences of this :term:`constant` are replaced by its extracted :term:`body`,
+    and this :term:`constant` is not declared in the generated file.
 
-  * If no inlining decision is taken, the constant is normally
+  * If no inlining decision is taken, the :term:`constant` is normally
     declared in the produced file. 
 
 Extra elimination of useless arguments
@@ -264,7 +264,7 @@ what ML term corresponds to a given axiom.
 
 .. cmd:: Extract Constant @qualid {* @string__tv } => {| @ident | @string }
 
-   Give an ML extraction for the given constant.
+   Give an ML extraction for the given :term:`constant`.
 
    :n:`@string__tv`
      If the type scheme axiom is an arity (a sequence of products followed
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 9ac05fab2e..930d286010 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -699,7 +699,7 @@ other. If a signature mentions a relation ``R`` on the left of an
 arrow ``==>``, then the signature also applies for any relation ``S`` that is
 smaller than ``R``, and the inverse applies on the right of an arrow. One
 can then declare only a few morphisms instances that generate the
-complete set of signatures for a particular constant. By default, the
+complete set of signatures for a particular :term:`constant`. By default, the
 only declared subrelation is ``iff``, which is a subrelation of ``impl`` and
 ``inverse impl`` (the dual of implication). That’s why we can declare only
 two morphisms for conjunction: ``Proper (impl ==> impl ==> impl) and`` and
@@ -714,8 +714,8 @@ example of a mostly user-space extension of the algorithm.
 Constant unfolding
 ~~~~~~~~~~~~~~~~~~
 
-The resolution tactic is based on typeclasses and hence regards user-
-defined constants as transparent by default. This may slow down the
+The resolution tactic is based on typeclasses and hence regards user-defined
+:term:`constants <constant>` as transparent by default. This may slow down the
 resolution due to a lot of unifications (all the declared ``Proper``
 instances are tried at each node of the search tree). To speed it up,
 declare your constant as rigid for proof search using the command
@@ -901,7 +901,7 @@ Hint databases created for :tacn:`autorewrite` can also be used
 by :tacn:`rewrite_strat` using the ``hints`` strategy that applies any of the
 lemmas at the current subterm. The ``terms`` strategy takes the lemma
 names directly as arguments. The ``eval`` strategy expects a reduction
-expression (see :ref:`performingcomputations`) and succeeds
+expression (see :ref:`applyingconversionrules`) and succeeds
 if it reduces the subterm under consideration. The ``fold`` strategy takes
 a :token:`term` and tries to *unify* it to the current subterm, converting it to :token:`term`
 on success. It is stronger than the tactic ``fold``.
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 09b2bb003a..c1b2200741 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -190,7 +190,7 @@ Use :n:`:>` instead of :n:`:` before the
 .. cmd:: Identity Coercion @ident : @class >-> @class
 
    If ``C`` is the source `class` and ``D`` the destination, we check
-   that ``C`` is a constant with a body of the form
+   that ``C`` is a :term:`constant` with a :term:`body` of the form
    :g:`fun (x₁:T₁)..(xₙ:Tₙ) => D t₁..tₘ` where `m` is the
    number of parameters of ``D``.  Then we define an identity
    function with type :g:`forall (x₁:T₁)..(xₙ:Tₙ)(y:C x₁..xₙ),D t₁..tₘ`,
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index 7d30cae525..8d70ffec01 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -15,12 +15,12 @@ it provides the following command:
    standing for the existential variables but they are shelved, as
    described in :tacn:`shelve`).
 
-   When the proof ends two constants are defined:
+   When the proof ends two :term:`constants <constant>` are defined:
 
    + The first one is named :n:`@ident__1` and is defined as the proof of the
      shelved goal (which is also the value of :g:`?x`). It is always
      transparent.
-   + The second one is named :n:`@ident__2`. It has type :n:`@type`, and its body is
+   + The second one is named :n:`@ident__2`. It has type :n:`@type`, and its :term:`body` is
      the proof of the initially visible goal. It is opaque if the proof
      ends with :cmd:`Qed`, and transparent if the proof ends with :cmd:`Defined`.
 
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 0997c5e868..86bb0502c6 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -147,7 +147,7 @@ Options
 
 .. flag:: Omega UseLocalDefs
 
-   This flag (on by default) allows :tacn:`omega` to use the bodies of local
+   This flag (on by default) allows :tacn:`omega` to use the :term:`bodies <body>` of local
    variables.
 
 .. flag:: Omega System
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 8f2b51ccce..a011c81f15 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -149,7 +149,7 @@ when reasoning with equality on the subset types themselves.
 
 The next two commands are similar to their standard counterparts
 :cmd:`Definition` and :cmd:`Fixpoint`
-in that they define constants. However, they may require the user to
+in that they define :term:`constants <constant>`. However, they may require the user to
 prove some goals to construct the final definitions.
 
 
@@ -173,7 +173,7 @@ term :n:`@term__0`, checking that the type of :n:`@term__0` is coercible to
 set of obligations generated during the interpretation of :n:`@term__0`
 and the aforementioned coercion derivation are solved.
 
-.. seealso:: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold`
+.. seealso:: Sections :ref:`controlling-the-reduction-strategies`, :tacn:`unfold`
 
 .. _program_fixpoint:
 
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 954c2c1446..6b7b588137 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -1,4 +1,4 @@
-.. |bdi| replace:: :math:`\beta\delta\iota`
+.. |bdi| replace:: βδι
 .. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}`
 .. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}`
 .. |eq| replace:: `=`:sub:`(by the main correctness theorem)`
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 8c20e08154..281473231d 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -44,7 +44,7 @@ are convertible:
    exact Hx.
    Qed.
 
-Since we have definitional :ref:`eta-expansion` for
+Since we have definitional :ref:`eta-expansion-sect` for
 functions, the property of being a type of definitionally irrelevant
 values is impredicative, and so is :math:`\SProp`:
 
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 8dc0030115..45741b4bb8 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -315,7 +315,7 @@ Summary of the commands
    inside records, and the trivial projection of an instance of such a
    class is convertible to the instance itself. This can be useful to
    make instances of existing objects easily and to reduce proof size by
-   not inserting useless projections. The class constant itself is
+   not inserting useless projections. The class :term:`constant` itself is
    declared rigid during resolution so that the class abstraction is
    maintained.
 
@@ -326,7 +326,7 @@ Summary of the commands
 
    .. cmd:: Existing Class @qualid
 
-      This variant declares a class from a previously declared constant or
+      This variant declares a class from a previously declared :term:`constant` or
       inductive definition. No methods or instances are defined.
 
       .. warn:: @ident is already declared as a typeclass
@@ -363,7 +363,7 @@ Summary of the commands
 
       This attribute can be used to leave holes or not provide all
       fields in the definition of an instance and open the tactic mode
-      to fill them.  It works exactly as if no body had been given and
+      to fill them.  It works exactly as if no :term:`body` had been given and
       the :tacn:`refine` tactic has been used first.
 
    .. cmd:: Declare Instance @ident_decl {* @binder } : @term {? @hint_info }
@@ -377,7 +377,7 @@ Summary of the commands
    .. cmd:: Existing Instance @qualid {? @hint_info }
             Existing Instances {+ @qualid } {? %| @natural }
 
-      Adds a constant whose type ends with
+      Adds a :term:`constant` whose type ends with
       an applied typeclass to the instance database with an optional
       priority :token:`natural`.  It can be used for redeclaring instances at the end of
       sections, or declaring structure projections as instances. This is
@@ -418,7 +418,7 @@ Summary of the commands
      unifier. When considering local hypotheses, we use the transparent
      state of the first hint database given. Using an empty database
      (created with :cmd:`Create HintDb` for example) with unfoldable variables and
-     constants as the first argument of ``typeclasses eauto`` hence makes
+     :term:`constants <constant>` as the first argument of ``typeclasses eauto`` hence makes
      resolution with the local hypotheses use full conversion during
      unification.
 
@@ -494,7 +494,7 @@ Typeclasses Transparent, Typeclasses Opaque
    Make :token:`qualid` opaque for typeclass search.
    A shortcut for :cmd:`Hint Opaque` :n:`{+ @qualid } : typeclass_instances`.
 
-   It is useful when some constants prevent some unifications and make
+   It is useful when some :term:`constants <constant>` prevent some unifications and make
    resolution fail. It is also useful to declare constants which
    should never be unfolded during proof search, like fixpoints or
    anything which does not look like an abbreviation. This can
@@ -502,7 +502,7 @@ Typeclasses Transparent, Typeclasses Opaque
    indexed by such rigid constants (see
    :ref:`thehintsdatabasesforautoandeauto`).
 
-By default, all constants and local variables are considered transparent. One
+By default, all :term:`constants <constant>` and local variables are considered transparent. One
 should take care not to make opaque any constant that is used to abbreviate a
 type, like:
 
@@ -531,7 +531,7 @@ Settings
    *unify* the goal with the conclusion of the hint. This can drastically
    improve performance by calling unification less often, matching
    syntactic patterns being very quick. This also provides more control
-   on the triggering of instances. For example, forcing a constant to
+   on the triggering of instances. For example, forcing a :term:`constant` to
    explicitly appear in the pattern will make it never apply on a goal
    where there is a hole in that place.
 
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index d0b05a03f9..773567b803 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -24,7 +24,7 @@ and *monomorphic* definitions is given by the identity function:
 
    Definition identity {A : Type} (a : A) := a.
 
-By default, constant declarations are monomorphic, hence the identity
+By default, :term:`constant` declarations are monomorphic, hence the identity
 function declares a global universe (say ``Top.1``) for its domain.
 Subsequently, if we try to self-apply the identity, we will get an
 error:
@@ -150,7 +150,7 @@ Polymorphic, Monomorphic
    attribute is used to override the default.
 
 Many other commands can be used to declare universe polymorphic or
-monomorphic constants depending on whether the :flag:`Universe
+monomorphic :term:`constants <constant>` depending on whether the :flag:`Universe
 Polymorphism` flag is on or the :attr:`universes(polymorphic)`
 attribute is used:
 
@@ -341,13 +341,13 @@ Conversion and unification
 The semantics of conversion and unification have to be modified a
 little to account for the new universe instance arguments to
 polymorphic references. The semantics respect the fact that
-definitions are transparent, so indistinguishable from their bodies
+definitions are transparent, so indistinguishable from their :term:`bodies <body>`
 during conversion.
 
 This is accomplished by changing one rule of unification, the first-
 order approximation rule, which applies when two applicative terms
 with the same head are compared. It tries to short-cut unfolding by
-comparing the arguments directly. In case the constant is universe
+comparing the arguments directly. In case the :term:`constant` is universe
 polymorphic, we allow this rule to fire only when unifying the
 universes results in instantiating a so-called flexible universe
 variables (not given by the user). Similarly for conversion, if such
@@ -362,7 +362,7 @@ Minimization
 
 Universe polymorphism with cumulativity tends to generate many useless
 inclusion constraints in general. Typically at each application of a
-polymorphic constant :g:`f`, if an argument has expected type :g:`Type@{i}`
+polymorphic :term:`constant` :g:`f`, if an argument has expected type :g:`Type@{i}`
 and is given a term of type :g:`Type@{j}`, a :math:`j ≤ i` constraint will be
 generated. It is however often the case that an equation :math:`j = i` would
 be more appropriate, when :g:`f`\'s universes are fresh for example.
@@ -550,7 +550,7 @@ underscore or by omitting the annotation to a polymorphic definition.
 .. flag:: Private Polymorphic Universes
 
    This flag, on by default, removes universes which appear only in
-   the body of an opaque polymorphic definition from the definition's
+   the :term:`body` of an opaque polymorphic definition from the definition's
    universe arguments. As such, no value needs to be provided for
    these universes when instantiating the definition. Universe
    constraints are automatically adjusted.
@@ -563,18 +563,18 @@ underscore or by omitting the annotation to a polymorphic definition.
       Proof. exact Type. Qed.
       Print foo.
 
-   The universe :g:`Top.xxx` for the :g:`Type` in the body cannot be accessed, we
+   The universe :g:`Top.xxx` for the :g:`Type` in the :term:`body` cannot be accessed, we
    only care that one exists for any instantiation of the universes
    appearing in the type of :g:`foo`. This is guaranteed when the
    transitive constraint ``Set <= Top.xxx < i`` is verified. Then when
-   using the constant we don't need to put a value for the inner
+   using the :term:`constant` we don't need to put a value for the inner
    universe:
 
    .. coqtop:: all
 
       Check foo@{_}.
 
-   and when not looking at the body we don't mention the private
+   and when not looking at the :term:`body` we don't mention the private
    universe:
 
    .. coqtop:: all
@@ -643,11 +643,11 @@ sections, except in the following ways:
   (in the above example the anonymous :g:`Type` constrains polymorphic
   universe :g:`i` to be strictly smaller.)
 
-- no monomorphic constant or inductive may be declared if polymorphic
+- no monomorphic :term:`constant` or inductive may be declared if polymorphic
   universes or universe constraints are present.
 
 These restrictions are required in order to produce a sensible result
-when closing the section (the requirement on constants and inductives
+when closing the section (the requirement on :term:`constants <constant>` and inductive types
 is stricter than the one on constraints, because constants and
 inductives are abstracted by *all* the section's polymorphic universes
 and constraints).
author	Jim Fehrle	2020-09-12 20:54:22 -0700
committer	Jim Fehrle	2021-03-08 11:48:20 -0800
commit	0d33024ff79c38d52fde49e23d0e45d9c22eefbe (patch)
tree	864068cd317abebcbc0a3466a1365258729fbc40 /doc/sphinx/addendum
parent	fb0666d50e1fe95ad2325f4ef2cc9fdd2666ac8a (diff)