Convert rewriting and proof-mode chapters to prodn

9 files changed, 93 insertions, 86 deletions

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.