Convert rewriting and proof-mode chapters to prodn

11 files changed, 15 insertions, 36 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 3662822a5e..8e72bb4ffd 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -100,7 +100,6 @@ Setting the target language
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. cmd:: Extraction Language @language
-   :name: Extraction Language
 
    .. insertprodn language language
 
@@ -431,12 +430,10 @@ Additional settings
 ~~~~~~~~~~~~~~~~~~~
 
 .. opt:: Extraction File Comment @string
-   :name: Extraction File Comment
 
    Provides a comment that is included at the beginning of the output files.
 
 .. opt:: Extraction Flag @natural
-   :name: Extraction Flag
 
    Controls which optimizations are used during extraction, providing a finer-grained
    control than :flag:`Extraction Optimize`.  The bits of :token:`natural` are used as a bit mask.
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 039a23e8c2..c54db36691 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -101,7 +101,7 @@ morphisms, that are required to be simultaneously monotone on every
 argument.
 
 Morphisms can also be contravariant in one or more of their arguments.
-A morphism is contravariant on an argument associated to the relation
+A morphism is contravariant on an argument associated with the relation
 instance :math:`R` if it is covariant on the same argument when the inverse
 relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->``
 is used in signatures for contravariant morphisms.
@@ -336,7 +336,7 @@ respective relation instances.
    in the previous example). Applying ``union_compat`` by hand we are left with the
    goal ``eq_set (union S S) (union S S)``.
 
-When the relations associated to some arguments are not reflexive, the
+When the relations associated with some arguments are not reflexive, the
 tactic cannot automatically prove the reflexivity goals, that are left
 to the user.
 
@@ -477,8 +477,8 @@ documentation on :ref:`typeclasses` and the theories files in Classes
 for further explanations.
 
 One can inform the rewrite tactic about morphisms and relations just
-by using the typeclass mechanism to declare them using Instance and
-Context vernacular commands. Any object of type Proper (the type of
+by using the typeclass mechanism to declare them using the :cmd:`Instance` and
+:cmd:`Context` commands. Any object of type Proper (the type of
 morphism declarations) in the local context will also be automatically
 used by the rewriting tactic to solve constraints.
 
@@ -553,7 +553,7 @@ pass additional arguments such as ``using relation``.
    be used to replace the first tactic argument with the second one. If
    omitted, it defaults to the ``DefaultRelation`` instance on the type of
    the objects. By default, it means the most recent ``Equivalence`` instance
-   in the environment, but it can be customized by declaring
+   in the global environment, but it can be customized by declaring
    new ``DefaultRelation`` instances. As Leibniz equality is a declared
    equivalence, it will fall back to it if no other relation is declared
    on a given type.
@@ -608,7 +608,6 @@ Deprecated syntax and backward incompatibilities
    an old development to the new semantics is usually quite simple.
 
 .. cmd:: Declare Morphism @one_term : @ident
-   :name: Declare Morphism
 
    Declares a parameter in a module type that is a morphism.
 
@@ -686,7 +685,7 @@ Note that when one does rewriting with a lemma under a binder using
 variable, as the semantics are different from rewrite where the lemma
 is first matched on the whole term. With the new :tacn:`setoid_rewrite`,
 matching is done on each subterm separately and in its local
-environment, and all matches are rewritten *simultaneously* by
+context, and all matches are rewritten *simultaneously* by
 default. The semantics of the previous :tacn:`setoid_rewrite` implementation
 can almost be recovered using the ``at 1`` modifier.
 
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 0f0ccd6a20..09b2bb003a 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -202,7 +202,6 @@ Use :n:`:>` instead of :n:`:` before the
       :undocumented:
 
    .. cmd:: SubClass @ident_decl @def_body
-      :name: SubClass
 
       If :n:`@type` is a class :n:`@ident'` applied to some arguments then
       :n:`@ident` is defined and an identity coercion of name
@@ -243,7 +242,6 @@ Activating the Printing of Coercions
    By default, coercions are not printed.
 
 .. table:: Printing Coercion @qualid
-   :name: Printing Coercion
 
    Specifies a set of qualids for which coercions are always displayed.  Use the
    :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids.
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 28b60878d2..38c4886e0f 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -140,7 +140,6 @@ and checked to be :math:`-1`.
 -------------------------------------------------------------------
 
 .. tacn:: lra
-   :name: lra
 
    This tactic is searching for *linear* refutations. As a result, this tactic explores a subset of the *Cone*
    defined as
@@ -154,7 +153,6 @@ and checked to be :math:`-1`.
 ---------------------------------------------
 
 .. tacn:: lia
-   :name: lia
 
    This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes.
    :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic.
@@ -220,7 +218,6 @@ a proof.
 --------------------------------------------------
 
 .. tacn:: nra
-   :name: nra
 
    This tactic is an *experimental* proof procedure for non-linear
    arithmetic. The tactic performs a limited amount of non-linear
@@ -241,7 +238,6 @@ proof by abstracting monomials by variables.
 ----------------------------------------------------------
 
 .. tacn:: nia
-   :name: nia
 
    This tactic is a proof procedure for non-linear integer arithmetic.
    It performs a pre-processing similar to :tacn:`nra`. The obtained goal is
@@ -251,7 +247,6 @@ proof by abstracting monomials by variables.
 ----------------------------------------------------
 
 .. tacn:: psatz @one_term {? @nat_or_var }
-   :name: psatz
 
    This tactic explores the *Cone* by increasing degrees – hence the
    depth parameter :token:`nat_or_var`. In theory, such a proof search is complete – if the
@@ -281,7 +276,6 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 ------------------------------------------
 
 .. tacn:: zify
-   :name: zify
 
    This tactic is internally called by :tacn:`lia` to support additional types, e.g., :g:`nat`, :g:`positive` and :g:`N`.
    Additional support is provided by the following modules:
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 2b10f5671d..0997c5e868 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -28,7 +28,6 @@ Description of ``omega``
 ------------------------
 
 .. tacn:: omega
-   :name: omega
 
    .. deprecated:: 8.12
 
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
index e824ae152d..ea506cec84 100644
--- a/doc/sphinx/addendum/parallel-proof-processing.rst
+++ b/doc/sphinx/addendum/parallel-proof-processing.rst
@@ -70,7 +70,7 @@ Coq 8.6 introduced a mechanism for error resilience: in interactive
 mode Coq is able to completely check a document containing errors
 instead of bailing out at the first failure.
 
-Two kind of errors are supported: errors occurring in vernacular
+Two kind of errors are supported: errors occurring in
 commands and errors occurring in proofs.
 
 To properly recover from a failing tactic, Coq needs to recognize the
@@ -89,8 +89,8 @@ kind of proof blocks, and an ML API to add new ones.
 Caveats
 ````````
 
-When a vernacular command fails the subsequent error messages may be
-bogus, i.e. caused by the first error. Error resilience for vernacular
+When a command fails the subsequent error messages may be
+bogus, i.e. caused by the first error. Error resilience for
 commands can be switched off by passing ``-async-proofs-command-error-resilience off``
 to CoqIDE.
 
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 104f84a253..2b24ced8a1 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -161,7 +161,7 @@ Program Definition
 A :cmd:`Definition` command with the :attr:`program` attribute types
 the value term in Russell and generates proof
 obligations. Once solved using the commands shown below, it binds the
-final Coq term to the name :n:`@ident` in the environment.
+final Coq term to the name :n:`@ident` in the global environment.
 
 :n:`Program Definition @ident : @type := @term`
 
@@ -268,7 +268,6 @@ obligations (e.g. when defining mutually recursive blocks). The
 optional tactic is replaced by the default one if not specified.
 
 .. cmd:: Obligation Tactic := @ltac_expr
-   :name: Obligation Tactic
 
    Sets the default obligation solving tactic applied to all obligations
    automatically, whether to solve them or when starting to prove one,
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index c93d621048..954c2c1446 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -421,7 +421,7 @@ Error messages:
 
 .. exn:: Ring operation should be declared as a morphism.
 
-  A setoid associated to the carrier of the ring structure has been found, 
+  A setoid associated with the carrier of the ring structure has been found,
   but the ring operation should be declared as morphism. See :ref:`tactics-enabled-on-user-provided-relations`.
 
 How does it work?
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 2b1f343e14..8c20e08154 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -19,7 +19,6 @@ Use of |SProp| may be disabled by passing ``-disallow-sprop`` to the
 Coq program or by turning the :flag:`Allow StrictProp` flag off.
 
 .. flag:: Allow StrictProp
-   :name: Allow StrictProp
 
    Enables or disables the use of |SProp|.  It is enabled by default.
    The command-line flag ``-disallow-sprop`` disables |SProp| at
@@ -283,7 +282,6 @@ This means that some errors will be delayed until ``Qed``:
    Abort.
 
 .. flag:: Elaboration StrictProp Cumulativity
-   :name: Elaboration StrictProp Cumulativity
 
    Unset this flag (it is on by default) to be strict with regard to
    :math:`\SProp` cumulativity during elaboration.
@@ -320,7 +318,6 @@ so correctly converts ``x`` and ``y``.
   it to find when your tactics are producing incorrect marks.
 
 .. flag:: Cumulative StrictProp
-   :name: Cumulative StrictProp
 
    Set this flag (it is off by default) to make the kernel accept
    cumulativity between |SProp| and other universes. This makes
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 4143d836c4..8dc0030115 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -160,7 +160,7 @@ Sections and contexts
 ---------------------
 
 To ease developments parameterized by many instances, one can use the
-:cmd:`Context` command to introduce these parameters into section contexts,
+:cmd:`Context` command to introduce the parameters into the :term:`local context`,
 it works similarly to the command :cmd:`Variable`, except it accepts any
 binding context as an argument, so variables can be implicit, and
 :ref:`implicit-generalization` can be used.
@@ -422,7 +422,7 @@ Summary of the commands
      resolution with the local hypotheses use full conversion during
      unification.
 
-   + The mode hints (see :cmd:`Hint Mode`) associated to a class are
+   + The mode hints (see :cmd:`Hint Mode`) associated with a class are
      taken into account by :tacn:`typeclasses eauto`. When a goal
      does not match any of the declared modes for its head (if any),
      instead of failing like :tacn:`eauto`, the goal is suspended and
@@ -470,7 +470,6 @@ Summary of the commands
         refinement engine will be able to backtrack.
 
 .. tacn:: autoapply @one_term with @ident
-   :name: autoapply
 
    The tactic ``autoapply`` applies :token:`one_term` using the transparency information
    of the hint database :token:`ident`, and does *no* typeclass resolution. This can
@@ -590,7 +589,6 @@ Settings
    :cmd:`Typeclasses eauto` is another way to set this flag.
 
 .. opt:: Typeclasses Depth @natural
-   :name: Typeclasses Depth
 
    Sets the maximum proof search depth.  The default is unbounded.
    :cmd:`Typeclasses eauto` is another way to set this option.
@@ -602,7 +600,6 @@ Settings
    is another way to set this flag.
 
 .. opt:: Typeclasses Debug Verbosity @natural
-   :name: Typeclasses Debug Verbosity
 
    Determines how much information is shown for typeclass resolution steps during search.
    1 is the default level.  2 shows additional information such as tried tactics and shelving
@@ -613,7 +610,6 @@ Typeclasses eauto
 ~~~~~~~~~~~~~~~~~
 
 .. cmd:: Typeclasses eauto := {? debug } {? ( {| bfs | dfs } ) } {? @natural }
-   :name: Typeclasses eauto
 
    Allows more global customization of the :tacn:`typeclasses eauto` tactic.
    The options are:
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index bb78b142ca..d0b05a03f9 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -328,7 +328,7 @@ Cumulativity Weak Constraints
 Global and local universes
 ---------------------------
 
-Each universe is declared in a global or local environment before it
+Each universe is declared in a global or local context before it
 can be used. To ensure compatibility, every *global* universe is set
 to be strictly greater than :g:`Set` when it is introduced, while every
 *local* (i.e. polymorphically quantified) universe is introduced as
@@ -617,7 +617,7 @@ definitions in the section sharing a common variable will both get
 parameterized by the universes produced by the variable declaration.
 This is in contrast to a “mononorphic” variable which introduces
 global universes and constraints, making the two definitions depend on
-the *same* global universes associated to the variable.
+the *same* global universes associated with the variable.
 
 It is possible to mix universe polymorphism and monomorphism in
 sections, except in the following ways: