Merge PR #13470: Convert rewriting and proof-mode chapters to prodn

Reviewed-by: Zimmi48
Ack-by: JasonGross

1 files changed, 56 insertions, 45 deletions

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.