Convert rewriting and proof-mode chapters to prodn

5 files changed, 10 insertions, 10 deletions

diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index d178311b4c..214541570c 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -4,7 +4,6 @@ Setting properties of a function's arguments
 ++++++++++++++++++++++++++++++++++++++++++++
 
 .. cmd:: Arguments @reference {* @arg_specs } {* , {* @implicits_alt } } {? : {+, @args_modifier } }
-   :name: Arguments
 
    .. insertprodn argument_spec args_modifier
 
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index aa754ab63d..4cc35794cc 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -199,8 +199,8 @@ but also that the infix relation was bound to the ``nat_eq`` relation.
 This relation is selected whenever ``==`` is used on terms of type nat.
 This can be read in the line declaring the canonical structure
 ``nat_EQty``, where the first argument to ``Pack`` is the key and its second
-argument a group of canonical values associated to the key. In this
-case we associate to nat only one canonical value (since its class,
+argument a group of canonical values associated with the key. In this
+case we associate with nat only one canonical value (since its class,
 ``nat_EQcl`` has just one member). The use of the projection ``op`` requires
 its argument to be in the class ``EQ``, and uses such a member (function)
 to actually compare its arguments.
@@ -530,7 +530,7 @@ instances of the ``LEQ`` class.
 
 The object ``Pack`` takes a type ``T`` (the key) and a mixin ``m``. It infers all
 the other pieces of the class ``LEQ`` and declares them as canonical
-values associated to the ``T`` key. All in all, the only new piece of
+values associated with the ``T`` key. All in all, the only new piece of
 information we add in the ``LEQ`` class is the mixin, all the rest is
 already canonical for ``T`` and hence can be inferred by Coq.
 
diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst
index fd9695e270..7206fb8581 100644
--- a/doc/sphinx/language/extensions/evars.rst
+++ b/doc/sphinx/language/extensions/evars.rst
@@ -5,6 +5,9 @@
 Existential variables
 ---------------------
 
+:gdef:`Existential variables <existential variable>` represent as yet unknown
+values.
+
 .. insertprodn term_evar term_evar
 
 .. prodn::
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index 23ba5f703a..765d04ec88 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -66,7 +66,7 @@ would be a solution of the inference problem.
 **Contextual Implicit Arguments**
 
 An implicit argument can be *contextual* or not. An implicit argument
-is said *contextual* if it can be inferred only from the knowledge of
+is said to be *contextual* if it can be inferred only from the knowledge of
 the type of the context of the current expression. For instance, the
 only argument of::
 
@@ -384,7 +384,7 @@ Displaying implicit arguments when pretty-printing
 
 .. flag:: Printing Implicit
 
-   By default, the basic pretty-printing rules hide the inferrable implicit
+   By default, the basic pretty-printing rules hide the inferable implicit
    arguments of an application. Turn this flag on to force printing all
    implicit arguments.
 
@@ -506,7 +506,7 @@ or :g:`m` to the type :g:`nat` of natural numbers).
 .. flag:: Printing Use Implicit Types
 
   By default, the type of bound variables is not printed when
-  the variable name is associated to an implicit type which matches the
+  the variable name is associated with an implicit type which matches the
   actual type of the variable. This feature can be deactivated by
   turning this flag off.
 
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 8e62c2af13..1c022448b0 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -252,7 +252,6 @@ If an inductive type has just one constructor, pattern matching can be
 written using the first destructuring let syntax.
 
 .. table:: Printing Let @qualid
-   :name: Printing Let
 
    Specifies a set of qualids for which pattern matching is displayed using a let expression.
    Note that this only applies to pattern matching instances entered with :g:`match`.
@@ -269,7 +268,6 @@ can be written using ``if`` … ``then`` … ``else`` ….  This table controls
 which types are written this way:
 
 .. table:: Printing If @qualid
-   :name: Printing If
 
    Specifies a set of qualids for which pattern matching is displayed using
    ``if`` … ``then`` … ``else`` ….  Use the :cmd:`Add` and :cmd:`Remove`
@@ -720,7 +718,7 @@ Recall that a list of patterns is also a pattern. So, when we
 destructure several terms at the same time and the branches have
 different types we need to provide the elimination predicate for this
 multiple pattern. It is done using the same scheme: each term may be
-associated to an ``as`` clause and an ``in`` clause in order to introduce
+associated with an ``as`` clause and an ``in`` clause in order to introduce
 a dependent product.
 
 For example, an equivalent definition for :g:`concat` (even though the