[Manual] Gather section-specific commands in Section documentation (fix #9704)

2 files changed, 50 insertions, 31 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 59506a6ff2..f2d305f4bc 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -768,7 +768,7 @@ 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.
@@ -805,6 +805,45 @@ Section :ref:`gallina-definitions`).
    Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which
    appear inside a section are canceled when the section is closed.
 
+.. cmd:: Variable @ident : @type
+
+   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*).
+   The :cmd:`Variable` command out of any section is equivalent to :cmd:`Local Parameter`.
+
+   .. exn:: @ident already exists.
+      :name: @ident already exists. (Variable)
+      :undocumented:
+
+   .. cmdv:: Variable {+ @ident } : @term
+
+      Links :token:`type` to each :token:`ident`.
+
+   .. 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) }`.
+
+.. cmd:: Context @binders
+
+   Declare variables in the context of the current section, like :cmd:`Variable`,
+   but also allowing implicit variables and :ref:`implicit-generalization`.
+
+   .. coqdoc::
+
+     Context {A : Type} (a b : A).
+     Context `{EqDec A}.
+
+   See also :ref:`contexts` in the chapter :ref:`typeclasses`.
 
 Module system
 -------------
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 158a3f5ffc..1c6fb4b193 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -630,36 +630,16 @@ has type :token:`type`.
 
       These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`.
 
-.. cmd:: Variable @ident : @type
-
-   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`.
-
-   See also :cmd:`Context`, a variant of :cmd:`Variable` where variables can be
-   made implicit and allowing :ref:`implicit-generalization`.
-
-   .. exn:: @ident already exists.
-      :name: @ident already exists. (Variable)
-      :undocumented:
-
-   .. cmdv:: Variable {+ @ident } : @term
-
-      Links :token:`type` to each :token:`ident`.
-
-   .. 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) }`.
+   .. cmdv:: Variable  {+ ( {+ @ident } : @type ) }
+             Variables {+ ( {+ @ident } : @type ) }
+             Hypothesis {+ ( {+ @ident } : @type ) }
+             Hypotheses {+ ( {+ @ident } : @type ) }
+      :name: Variable-Parameter; Variables-Parameter; Hypothesis-Parameter; Hypotheses-Parameter
+
+      Out of any section, these variants are synonyms of
+      :n:`Local Parameter {+ ( {+ @ident } : @type ) }`.
+      For their meaning inside a section, see the documentation on
+      :ref:`section-mechanism`.
 
 .. note::
    It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and