Merge PR #9789: [Manual] Improve documentation on Section, Variable, Context

Reviewed-by: Zimmi48
Ack-by: jfehrle

2 files changed, 125 insertions, 76 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 59506a6ff2..18cafd1f21 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -754,10 +754,46 @@ used by ``Function``. A more precise description is given below.
 Section mechanism
 -----------------
 
-The sectioning mechanism can be used to to organize a proof in
-structured sections. Then local declarations become available (see
-Section :ref:`gallina-definitions`).
+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.
 
 .. cmd:: Section @ident
 
@@ -768,43 +804,80 @@ Section :ref:`gallina-definitions`).
 .. cmd:: End @ident
 
    This command closes the section named :token:`ident`. After closing of the
-   section, the local declarations (variables and local definitions) get
+   section, the local declarations (variables and local definitions, see :cmd:`Variable`) get
    *discharged*, meaning that they stop being visible and that all global
    objects defined in the section are generalized with respect to the
    variables and local definitions they each depended on in the section.
 
-   .. example::
+   .. exn:: This is not the last opened section.
+      :undocumented:
 
-      .. coqtop:: all
+.. note::
+   Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which
+   appear inside a section are canceled when the section is closed.
 
-         Section s1.
+.. cmd:: Variable @ident : @type
 
-         Variables x y : nat.
+   This command links :token:`type` to the name :token:`ident` in the context of
+   the current section. When the current section is closed, name :token:`ident`
+   will be unknown and every object using this variable will be explicitly
+   parameterized (the variable is *discharged*).
 
-         Let y' := y.
+   .. exn:: @ident already exists.
+      :name: @ident already exists. (Variable)
+      :undocumented:
 
-         Definition x' := S x.
+   .. cmdv:: Variable {+ @ident } : @type
 
-         Definition x'' := x' + y'.
+      Links :token:`type` to each :token:`ident`.
 
-         Print x'.
+   .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
 
-         End s1.
+      Declare one or more variables with various types.
 
-         Print x'.
+   .. cmdv:: Variables {+ ( {+ @ident } : @type) }
+             Hypothesis {+ ( {+ @ident } : @type) }
+             Hypotheses {+ ( {+ @ident } : @type) }
+      :name: Variables; Hypothesis; Hypotheses
 
-         Print x''.
+      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
 
-      Notice the difference between the value of :g:`x'` and :g:`x''` inside section
-      :g:`s1` and outside.
+.. cmd:: Let @ident := @term
 
-   .. exn:: This is not the last opened section.
+   This command binds the value :token:`term` to the name :token:`ident` in the
+   environment of the current section. The name :token:`ident` is accessible
+   only within the current section. When the section is closed, all persistent
+   definitions and theorems within it and depending on :token:`ident`
+   will be prefixed by the let-in definition :n:`let @ident := @term in`.
+
+   .. exn:: @ident already exists.
+      :name: @ident already exists. (Let)
       :undocumented:
 
-.. note::
-   Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which
-   appear inside a section are canceled when the section is closed.
+   .. cmdv:: Let @ident {? @binders } {? : @type } := @term
+      :undocumented:
+
+   .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body}
+      :name: Let Fixpoint
+      :undocumented:
+
+   .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body}
+      :name: Let CoFixpoint
+      :undocumented:
+
+.. cmd:: Context @binders
+
+   Declare variables in the context of the current section, like :cmd:`Variable`,
+   but also allowing implicit variables, :ref:`implicit-generalization`, and
+   let-binders.
+
+   .. coqdoc::
+
+     Context {A : Type} (a b : A).
+     Context `{EqDec A}.
+     Context (b' := b).
 
+.. seealso:: Section :ref:`binders`. Section :ref:`contexts` in chapter :ref:`typeclasses`.
 
 Module system
 -------------
@@ -2028,7 +2101,7 @@ or :g:`m` to the type :g:`nat` of natural numbers).
 
   This is useful for declaring the implicit type of a single variable.
 
-.. cmdv:: Implicit Types {+ ( {+ @ident } : @term ) }
+.. cmdv:: Implicit Types {+ ( {+ @ident } : @type ) }
 
   Adds blocks of implicit types with different specifications.
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 02fb9d84ce..8a5e9d87f8 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -630,33 +630,21 @@ has type :token:`type`.
 
       These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`.
 
-.. cmd:: Variable @ident : @type
+   .. cmdv:: Variable  {+ ( {+ @ident } : @type ) }
+             Variables {+ ( {+ @ident } : @type ) }
+             Hypothesis {+ ( {+ @ident } : @type ) }
+             Hypotheses {+ ( {+ @ident } : @type ) }
+      :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section)
 
-   This command links :token:`type` to the name :token:`ident` in the context of
-   the current section (see Section :ref:`section-mechanism` for a description of
-   the section mechanism). When the current section is closed, name :token:`ident`
-   will be unknown and every object using this variable will be explicitly
-   parametrized (the variable is *discharged*). Using the :cmd:`Variable` command out
-   of any section is equivalent to using :cmd:`Local Parameter`.
+      Outside of any section, these variants are synonyms of
+      :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
+      For their meaning inside a section, see :cmd:`Variable` in
+      :ref:`section-mechanism`.
 
-   .. exn:: @ident already exists.
-      :name: @ident already exists. (Variable)
-      :undocumented:
-
-   .. cmdv:: Variable {+ @ident } : @term
-
-      Links :token:`type` to each :token:`ident`.
+      .. warn:: @ident is declared as a local axiom [local-declaration,scope]
 
-   .. cmdv:: Variable {+ ( {+ @ident } : @term ) }
-
-      Adds blocks of variables with different specifications.
-
-   .. cmdv:: Variables {+ ( {+ @ident } : @term) }
-             Hypothesis {+ ( {+ @ident } : @term) }
-             Hypotheses {+ ( {+ @ident } : @term) }
-      :name: Variables; Hypothesis; Hypotheses
-
-      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @term) }`.
+         Warning generated when using :cmd:`Variable` instead of
+         :cmd:`Local Parameter`.
 
 .. note::
    It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and
@@ -665,6 +653,8 @@ has type :token:`type`.
    :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases
    (corresponding to the declaration of an abstract mathematical entity).
 
+.. seealso:: Section :ref:`section-mechanism`.
+
 .. _gallina-definitions:
 
 Definitions
@@ -704,10 +694,10 @@ Section :ref:`typing-rules`.
       .. exn:: The term @term has type @type while it is expected to have type @type'.
          :undocumented:
 
-   .. cmdv:: Definition @ident @binders {? : @term } := @term
+   .. cmdv:: Definition @ident @binders {? : @type } := @term
 
       This is equivalent to
-      :n:`Definition @ident : forall @binders, @term := fun @binders => @term`.
+      :n:`Definition @ident : forall @binders, @type := fun @binders => @term`.
 
    .. cmdv:: Local Definition @ident {? @binders } {? : @type } := @term
       :name: Local Definition
@@ -721,32 +711,18 @@ Section :ref:`typing-rules`.
 
       This is equivalent to :cmd:`Definition`.
 
-.. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
+   .. cmdv:: Let @ident := @term
+      :name: Let (outside a section)
 
-.. cmd:: Let @ident := @term
+      Outside of any section, this variant is a synonym of
+      :n:`Local Definition @ident := @term`.
+      For its meaning inside a section, see :cmd:`Let` in
+      :ref:`section-mechanism`.
 
-   This command binds the value :token:`term` to the name :token:`ident` in the
-   environment of the current section. The name :token:`ident` disappears when the
-   current section is eventually closed, and all persistent objects (such
-   as theorems) defined within the section and depending on :token:`ident` are
-   prefixed by the let-in definition :n:`let @ident := @term in`.
-   Using the :cmd:`Let` command out of any section is equivalent to using
-   :cmd:`Local Definition`.
+      .. warn:: @ident is declared as a local definition [local-declaration,scope]
 
-   .. exn:: @ident already exists.
-      :name: @ident already exists. (Let)
-      :undocumented:
-
-   .. cmdv:: Let @ident {? @binders } {? : @type } := @term
-      :undocumented:
-
-   .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body}
-      :name: Let Fixpoint
-      :undocumented:
-
-   .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body}
-      :name: Let CoFixpoint
-      :undocumented:
+         Warning generated when using :cmd:`Let` instead of
+         :cmd:`Local Definition`.
 
 .. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`,
              :cmd:`Transparent`, and tactic :tacn:`unfold`.
@@ -877,8 +853,8 @@ which is a type whose conclusion is a sort.
    successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the
    structural induction principle we got for :g:`nat`.
 
-Parametrized inductive types
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Parameterized inductive types
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. cmdv:: Inductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type}
 
@@ -954,7 +930,7 @@ Parametrized inductive types
      because the conclusion of the type of constructors should be :g:`listw A`
      in both cases.
 
-   + A parametrized inductive definition can be defined using annotations
+   + A parameterized inductive definition can be defined using annotations
      instead of parameters but it will sometimes give a different (bigger)
      sort for the inductive definition and will produce a less convenient
      rule for case elimination.
@@ -1014,7 +990,7 @@ Mutually defined inductive types
 
    .. cmdv:: Inductive @ident @binders {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident @binders {? : @type } } }
 
-      In this variant, the inductive definitions are parametrized
+      In this variant, the inductive definitions are parameterized
       with :token:`binders`. However, parameters correspond to a local context
       in which the whole set of inductive declarations is done. For this
       reason, the parameters must be strictly the same for each inductive types.
@@ -1050,7 +1026,7 @@ Mutually defined inductive types
 
       Check forest_rec.
 
-   Assume we want to parametrize our mutual inductive definitions with the
+   Assume we want to parameterize our mutual inductive definitions with the
    two type variables :g:`A` and :g:`B`, the declaration should be
    done the following way: