Convert rewriting and proof-mode chapters to prodn

16 files changed, 130 insertions, 128 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 85b04f6df0..1cfd8dac50 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -101,7 +101,7 @@ and it can be applied to any expression of type :math:`\nat`, say :math:`t`, to
 object :math:`P~t` of type :math:`\Prop`, namely a proposition.
 
 Furthermore :g:`forall x:nat, P x` will represent the type of functions
-which associate to each natural number :math:`n` an object of type :math:`(P~n)` and
+which associate with each natural number :math:`n` an object of type :math:`(P~n)` and
 consequently represent the type of proofs of the formula “:math:`∀ x.~P(x)`”.
 
 
@@ -111,51 +111,49 @@ Typing rules
 ----------------
 
 As objects of type theory, terms are subjected to *type discipline*.
-The well typing of a term depends on a global environment and a local
-context.
-
+The well typing of a term depends on a local context and a global environment.
 
 .. _Local-context:
 
 **Local context.**
-A *local context* is an ordered list of *local declarations* of names
-which we call *variables*. The declaration of some variable :math:`x` is
-either a *local assumption*, written :math:`x:T` (:math:`T` is a type) or a *local
-definition*, written :math:`x:=t:T`. We use brackets to write local contexts.
-A typical example is :math:`[x:T;~y:=u:U;~z:V]`. Notice that the variables
+A :term:`local context` is an ordered list of declarations of *variables*.
+The declaration of a variable :math:`x` is
+either an *assumption*, written :math:`x:T` (where :math:`T` is a type) or a
+*definition*, written :math:`x:=t:T`. Local contexts are written in brackets,
+for example :math:`[x:T;~y:=u:U;~z:V]`. The variables
 declared in a local context must be distinct. If :math:`Γ` is a local context
-that declares some :math:`x`, we
-write :math:`x ∈ Γ`. By writing :math:`(x:T) ∈ Γ` we mean that either :math:`x:T` is an
-assumption in :math:`Γ` or that there exists some :math:`t` such that :math:`x:=t:T` is a
-definition in :math:`Γ`. If :math:`Γ` defines some :math:`x:=t:T`, we also write :math:`(x:=t:T) ∈ Γ`.
+that declares :math:`x`, we
+write :math:`x ∈ Γ`. Writing :math:`(x:T) ∈ Γ` means there is an assumption
+or a definition giving the type :math:`T` to :math:`x` in :math:`Γ`.
+If :math:`Γ` defines :math:`x:=t:T`, we also write :math:`(x:=t:T) ∈ Γ`.
 For the rest of the chapter, :math:`Γ::(y:T)` denotes the local context :math:`Γ`
 enriched with the local assumption :math:`y:T`. Similarly, :math:`Γ::(y:=t:T)` denotes
 the local context :math:`Γ` enriched with the local definition :math:`(y:=t:T)`. The
-notation :math:`[]` denotes the empty local context. By :math:`Γ_1 ; Γ_2` we mean
+notation :math:`[]` denotes the empty local context. Writing :math:`Γ_1 ; Γ_2` means
 concatenation of the local context :math:`Γ_1` and the local context :math:`Γ_2`.
 
-
 .. _Global-environment:
 
 **Global environment.**
-A *global environment* is an ordered list of *global declarations*.
-Global declarations are either *global assumptions* or *global
-definitions*, but also declarations of inductive objects. Inductive
-objects themselves declare both inductive or coinductive types and
-constructors (see Section :ref:`inductive-definitions`).
-
-A *global assumption* will be represented in the global environment as
-:math:`(c:T)` which assumes the name :math:`c` to be of some type :math:`T`. A *global
-definition* will be represented in the global environment as :math:`c:=t:T`
-which defines the name :math:`c` to have value :math:`t` and type :math:`T`. We shall call
+A :term:`global environment` is an ordered list of *declarations*.
+Global declarations are either *assumptions*, *definitions*
+or declarations of inductive objects. Inductive
+objects declare both constructors and inductive or
+coinductive types (see Section :ref:`inductive-definitions`).
+
+In the global environment,
+*assumptions* are written as
+: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
-the global environment :math:`E` enriched with the global assumption :math:`c:T`.
+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
-global definition :math:`(c:=t:T)`.
+definition :math:`(c:=t:T)`.
 
 The rules for inductive definitions (see Section
 :ref:`inductive-definitions`) have to be considered as assumption
-rules to which the following definitions apply: if the name :math:`c`
+rules in which the following definitions apply: if the name :math:`c`
 is declared in :math:`E`, we write :math:`c ∈ E` and if :math:`c:T` or
 :math:`c:=t:T` is declared in :math:`E`, we write :math:`(c : T) ∈ E`.
 
@@ -315,7 +313,7 @@ following rules.
 .. note::
    We may have :math:`\letin{x}{t:T}{u}` well-typed without having
    :math:`((λ x:T.~u)~t)` well-typed (where :math:`T` is a type of
-   :math:`t`). This is because the value :math:`t` associated to
+   :math:`t`). This is because the value :math:`t` associated with
    :math:`x` may be used in a conversion rule
    (see Section :ref:`Conversion-rules`).
 
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index d061ed41f1..4f54e33758 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -902,7 +902,6 @@ In addition to the powerful ``ring``, ``field`` and ``lra``
 tactics (see Chapter :ref:`tactics`), there are also:
 
 .. tacn:: discrR
-  :name: discrR
 
   Proves that two real integer constants are different.
 
@@ -916,7 +915,6 @@ tactics (see Chapter :ref:`tactics`), there are also:
     discrR.
 
 .. tacn:: split_Rabs
-  :name: split_Rabs
 
   Allows unfolding the ``Rabs`` constant and splits corresponding conjunctions.
 
@@ -930,7 +928,6 @@ tactics (see Chapter :ref:`tactics`), there are also:
     intro; split_Rabs.
 
 .. tacn:: split_Rmult
-  :name: split_Rmult
 
   Splits a condition that a product is non null into subgoals
   corresponding to the condition on each operand of the product.
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index e86a6f4a67..8dbc1626ba 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -115,10 +115,10 @@ Section :ref:`explicit-applications`).
 Assumptions
 -----------
 
-Assumptions extend the environment with axioms, parameters, hypotheses
+Assumptions extend the global environment with axioms, parameters, hypotheses
 or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted
-by Coq if and only if this :n:`@type` is a correct type in the environment
-preexisting the declaration and if :n:`@ident` was not previously defined in
+by Coq only if :n:`@type` is a correct type in the global environment
+before the declaration and if :n:`@ident` was not previously defined in
 the same module. This :n:`@type` is considered to be the type (or
 specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident`
 has type :n:`@type`.
@@ -141,7 +141,7 @@ has type :n:`@type`.
       of_type ::= {| : | :> } @type
 
    These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in
-   the global context. The fact asserted by :n:`@type` (or, equivalently, the existence
+   the global environment. The fact asserted by :n:`@type` (or, equivalently, the existence
    of an object of this type) is accepted as a postulate.  They accept the :attr:`program` attribute.
 
    :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 2b262b89c0..0a61c4ce22 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -64,7 +64,7 @@ appending the level to the nonterminal name (as in :n:`@term100` or
    populated by notations or plugins.
 
    Furthermore, some parsing rules are only activated in certain
-   contexts (:ref:`interactive proof mode <proofhandling>`,
+   contexts (:ref:`proof mode <proofhandling>`,
    :ref:`custom entries <custom-entries>`...).
 
 .. warning::
@@ -332,9 +332,9 @@ rest of the Coq manual: :term:`terms <term>` and :term:`types
 
    tactic
 
-     Tactics specify how to transform the current proof state as a
+     A :production:`tactic` specifies how to transform the current proof state as a
      step in creating a proof.  They are syntactically valid only when
-     Coq is in proof mode, such as after a :cmd:`Theorem` command
+     Coq is in :term:`proof mode`, such as after a :cmd:`Theorem` command
      and before any subsequent proof-terminating command such as
      :cmd:`Qed`.  See :ref:`proofhandling` for more on proof mode.
 
@@ -450,7 +450,6 @@ they appear after a boldface label.  They are listed in the
 :ref:`options_index`.
 
 .. cmd:: Set @setting_name {? {| @integer | @string } }
-   :name: Set
 
    If :n:`@setting_name` is a flag, no value may be provided; the flag
    is set to on.
@@ -471,7 +470,6 @@ they appear after a boldface label.  They are listed in the
       Coq versions.
 
 .. cmd:: Unset @setting_name
-   :name: Unset
 
    If :n:`@setting_name` is a flag, it is set to off.  If :n:`@setting_name` is an option, it is
    set to its default value.
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index cf46580bdb..e742139134 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -194,7 +194,7 @@ Top-level definitions of co-recursive functions
    As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously
    defining several mutual cofixpoints.
 
-   If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
+   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
    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 7395b12339..09c619338b 100644
--- a/doc/sphinx/language/core/conversion.rst
+++ b/doc/sphinx/language/core/conversion.rst
@@ -47,7 +47,7 @@ refer the interested reader to :cite:`Coq85`.
 ι-reduction
 ~~~~~~~~~~~
 
-A specific conversion rule is associated to the inductive objects in
+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
@@ -159,7 +159,8 @@ relation :math:`t` reduces to :math:`u` in the global environment
 reductions β, δ, ι or ζ.
 
 We say that two terms :math:`t_1` and :math:`t_2` are
-*βδιζη-convertible*, or simply :gdef:`convertible`, or *equivalent*, in the
+*βδιζη-convertible*, or simply :gdef:`convertible`, or
+:term:`definitionally equal <definitional equality>`, in the
 global environment :math:`E` and local context :math:`Γ` iff there
 exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright
 … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 6da1f90ecb..7196c082ed 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -56,7 +56,7 @@ has type :n:`@type`.
 Top-level definitions
 ---------------------
 
-Definitions extend the environment with associations of names to terms.
+Definitions extend the global environment with associations of 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.
@@ -82,7 +82,7 @@ Section :ref:`typing-rules`.
       | {* @binder } : @type
       reduce ::= Eval @red_expr in
 
-   These commands bind :n:`@term` to the name :n:`@ident` in the environment,
+   These commands bind :n:`@term` to the name :n:`@ident` in the global environment,
    provided that :n:`@term` is well-typed.  They can take the :attr:`local` :term:`attribute`,
    which makes the defined :n:`@ident` accessible by :cmd:`Import` and its variants
    only through their fully qualified names.
@@ -94,7 +94,7 @@ Section :ref:`typing-rules`.
    :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, and
    :attr:`using` attributes.
 
-   If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
+   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
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
@@ -120,10 +120,11 @@ Section :ref:`typing-rules`.
 Assertions and proofs
 ---------------------
 
-An assertion states a proposition (or a type) of which the proof (or an
-inhabitant of the type) is interactively built using tactics. The interactive
-proof mode is described in Chapter :ref:`proofhandling` and the tactics in
-Chapter :ref:`Tactics`. The basic assertion command is:
+An assertion states a proposition (or a type) for which the proof (or an
+inhabitant of the type) is interactively built using :term:`tactics <tactic>`.
+Assertions cause Coq to enter :term:`proof mode` (see :ref:`proofhandling`).
+Common tactics are described in the :ref:`writing-proofs` chapter.
+The basic assertion command is:
 
 .. cmd:: @thm_token @ident_decl {* @binder } : @type {* with @ident_decl {* @binder } : @type }
    :name: Theorem; Lemma; Fact; Remark; Corollary; Proposition; Property
@@ -142,7 +143,7 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    After the statement is asserted, Coq needs a proof. Once a proof of
    :n:`@type` under the assumptions represented by :n:`@binder`\s is given and
    validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and
-   the theorem is bound to the name :n:`@ident` in the environment.
+   the theorem is bound to the name :n:`@ident` in the global environment.
 
    These commands accept the :attr:`program` attribute.  See :ref:`program_lemma`.
 
@@ -159,7 +160,7 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    have to be used on *structurally smaller* arguments (for a :cmd:`Fixpoint`) or
    be *guarded by a constructor* (for a :cmd:`CoFixpoint`). The verification that
    recursive proof arguments are correct is done only at the time of registering
-   the lemma in the environment. To know if the use of induction hypotheses is
+   the lemma in the global environment. To know if the use of induction hypotheses is
    correct at some time of the interactive development of a proof, use the
    command :cmd:`Guarded`.
 
@@ -178,25 +179,24 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    .. exn:: Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". \
             If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on.
 
-      You are asserting a new statement while already being in proof editing mode.
+      You are asserting a new statement when you're already in proof mode.
       This feature, called nested proofs, is disabled by default.
       To activate it, turn the :flag:`Nested Proofs Allowed` flag on.
 
-Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode
-until the proof is completed. In proof editing mode, the user primarily enters
-tactics, which are described in chapter :ref:`Tactics`. The user may also enter
-commands to manage the proof editing mode. They are described in Chapter
-:ref:`proofhandling`.
+Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof mode
+until the proof is completed. In proof mode, the user primarily enters
+tactics (see :ref:`writing-proofs`). The user may also enter
+commands to manage the proof mode (see :ref:`proofhandling`).
 
 When the proof is complete, use the :cmd:`Qed` command so the kernel verifies
-the proof and adds it to the environment.
+the proof and adds it to the global environment.
 
 .. note::
 
    #. Several statements can be simultaneously asserted provided the
       :flag:`Nested Proofs Allowed` flag was turned on.
 
-   #. Not only other assertions but any vernacular command can be given
+   #. Not only other assertions but any command can be given
       while in the process of proving a given assertion. In this case, the
       command is understood as if it would have been given before the
       statements still to be proved. Nonetheless, this practice is discouraged
@@ -211,4 +211,4 @@ the proof and adds it to the environment.
       side, :cmd:`Qed` (or :cmd:`Defined`) is mandatory to validate a proof.
 
    #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the
-      current asserted statement into an axiom and exit the proof editing mode.
+      current asserted statement into an axiom and exit proof mode.
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 4bee7cc1b1..4e892f709d 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -36,7 +36,7 @@ Inductive types
    :attr:`private(matching)` attributes.
 
    Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s.
-   The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked.
+   The :n:`@ident`\s are simultaneously added to the global environment before the types of constructors are checked.
    Each :n:`@ident` can be used independently thereafter.
    See :ref:`mutually_inductive_types`.
 
@@ -86,7 +86,7 @@ A simple inductive type belongs to a universe that is a simple :n:`@sort`.
 
    The type nat is defined as the least :g:`Set` containing :g:`O` and closed by
    the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the
-   environment.
+   global environment.
 
    This definition generates four elimination principles:
    :g:`nat_rect`, :g:`nat_ind`, :g:`nat_rec` and :g:`nat_sind`. The type of :g:`nat_ind` is:
@@ -413,7 +413,7 @@ constructions.
    It is especially useful when defining functions over mutually defined
    inductive types.  Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`.
 
-   If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
+   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
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
@@ -636,7 +636,7 @@ contains an inductive definition.
 
 .. example::
 
-   Provided that our environment :math:`E` contains inductive definitions we showed before,
+   Provided that our global environment :math:`E` contains inductive definitions we showed before,
    these two inference rules above enable us to conclude that:
 
    .. math::
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 6d96e15202..93d70c773f 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -283,7 +283,6 @@ are now available through the dot notation.
          Check A.B.U.
 
 .. cmd:: Export {+ @filtered_import }
-   :name: Export
 
    Similar to :cmd:`Import`, except that when the module containing this command
    is imported, the :n:`{+ @qualid }` are imported as well.
@@ -465,7 +464,7 @@ We also need additional typing judgments:
 
 + :math:`\WFT{E}{S}`, denoting that a structure :math:`S` is well-formed,
 + :math:`\WTM{E}{p}{S}`, denoting that the module pointed by :math:`p` has type :math:`S` in
-  environment :math:`E`.
+  the global environment :math:`E`.
 + :math:`\WEV{E}{S}{\ovl{S}}`, denoting that a structure :math:`S` is evaluated to a
   structure :math:`S` in weak head normal form.
 + :math:`\WS{E}{S_1}{S_2}` , denoting that a structure :math:`S_1` is a subtype of a
@@ -965,7 +964,7 @@ names.
 
 A logical prefix Lib can be associated with a physical path using
 the command line option ``-Q`` `path` ``Lib``. All subfolders of path are
-recursively associated to the logical path ``Lib`` extended with the
+recursively associated with the logical path ``Lib`` extended with the
 corresponding suffix coming from the physical path. For instance, the
 folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding
 to invalid Coq identifiers are skipped, and, by convention,
@@ -973,7 +972,7 @@ subdirectories named ``CVS`` or ``_darcs`` are skipped too.
 
 Thanks to this mechanism, ``.vo`` files are made available through the
 logical name of the folder they are in, extended with their own
-basename. For example, the name associated to the file
+basename. For example, the name associated with the file
 ``path/fOO/Bar/File.vo`` is ``Lib.fOO.Bar.File``. The same caveat applies for
 invalid identifiers. When compiling a source file, the ``.vo`` file stores
 its logical name, so that an error is issued if it is loaded with the
diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index 7eedbcd59a..6671c67fb2 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -119,13 +119,11 @@ The following settings let you control the display format for types:
 You can override the display format for specified types by adding entries to these tables:
 
 .. table:: Printing Record @qualid
-   :name: Printing Record
 
    Specifies a set of qualids which are displayed as records.  Use the
    :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids.
 
 .. table:: Printing Constructor @qualid
-   :name: Printing Constructor
 
    Specifies a set of qualids which are displayed as constructors.  Use the
    :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids.
@@ -208,7 +206,7 @@ other arguments are the parameters of the inductive type.
   This message is followed by an explanation of this impossibility.
   There may be three reasons:
 
-  #. The name :token:`ident` already exists in the environment (see :cmd:`Axiom`).
+  #. The name :token:`ident` already exists in the global environment (see :cmd:`Axiom`).
   #. The 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
diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
index 75389bb259..c16152ff4f 100644
--- a/doc/sphinx/language/core/sections.rst
+++ b/doc/sphinx/language/core/sections.rst
@@ -3,57 +3,33 @@
 Section mechanism
 -----------------
 
-Sections create local contexts which can be shared across multiple definitions.
-
-.. example::
-
-   Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`.
-
-   .. coqtop:: all
-
-      Section s1.
-
-   Inside a section, local parameters can be introduced using :cmd:`Variable`,
-   :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for
-   the first two).
-
-   .. coqtop:: all
-
-      Variables x y : nat.
-
-   The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions
-   won't persist when the section is closed, and all persistent definitions which
-   depend on `y'` will be prefixed with `let y' := y in`.
-
-   .. coqtop:: in
-
-      Let y' := y.
-      Definition x' := S x.
-      Definition x'' := x' + y'.
-
-   .. coqtop:: all
-
-      Print x'.
-      Print x''.
-
-      End s1.
-
-      Print x'.
-      Print x''.
-
-   Notice the difference between the value of :g:`x'` and :g:`x''` inside section
-   :g:`s1` and outside.
+Sections are naming scopes that permit creating section-local declarations that can
+be used by other declarations in the section.  Declarations made
+with :cmd:`Variable`, :cmd:`Hypothesis`, :cmd:`Context`,
+:cmd:`Let`, :cmd:`Let Fixpoint` and
+:cmd:`Let CoFixpoint` (or the plural variants of the first two) within sections
+are local to the section.
+
+In proofs done within the section, section-local declarations
+are included in the :term:`local context` of the initial goal of the proof.
+They are also accessible in definitions made with the :cmd:`Definition` command.
+
+Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`.
+Sections can be nested.
+When a section is closed, its local declarations are no longer available.
+Global declarations that refer to them will be adjusted so they're still
+usable outside the section as shown in this :ref:`example <section_local_declarations>`.
 
 .. cmd:: Section @ident
 
-   This command is used to open a section named :token:`ident`.
+   Opens the section named :token:`ident`.
    Section names do not need to be unique.
 
 
 .. cmd:: End @ident
 
-   This command closes the section or module named :token:`ident`.
-   See :ref:`Terminating an interactive module or module type definition<terminating_module>`
+   Closes the section or module named :token:`ident`.
+   See :ref:`Terminating an interactive module or module type definition <terminating_module>`
    for a description of its use with modules.
 
    After closing the
@@ -78,14 +54,14 @@ Sections create local contexts which can be shared across multiple definitions.
          Let CoFixpoint @cofix_definition {* with @cofix_definition }
    :name: Let; Let Fixpoint; Let CoFixpoint
 
-   These commands behave like :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, except that
+   These are similar to :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, except that
    the declared 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.
 
    As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`,
-   if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
+   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
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
@@ -103,3 +79,38 @@ Sections create local contexts which can be shared across multiple definitions.
      Context (b' := b).
 
 .. seealso:: Section :ref:`binders`. Section :ref:`contexts` in chapter :ref:`typeclasses`.
+
+.. _section_local_declarations:
+
+.. example:: Section-local declarations
+
+   .. coqtop:: all
+
+      Section s1.
+
+   .. coqtop:: all
+
+      Variables x y : nat.
+
+   The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions
+   won't persist when the section is closed, and all persistent definitions which
+   depend on `y'` will be prefixed with `let y' := y in`.
+
+   .. coqtop:: in
+
+      Let y' := y.
+      Definition x' := S x.
+      Definition x'' := x' + y'.
+
+   .. coqtop:: all
+
+      Print x'.
+      Print x''.
+
+      End s1.
+
+      Print x'.
+      Print x''.
+
+   Notice the difference between the value of :g:`x'` and :g:`x''` inside section
+   :g:`s1` and outside.
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