[Manual] Move command Context after Let, and more polishing

- Refine some `@term` into `@type`

3 files changed, 36 insertions, 35 deletions

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 60b346c211..e6a5b3972c 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -146,10 +146,10 @@ database.
 Sections and contexts
 ---------------------
 
-To ease the parametrization of developments by typeclasses, one can use
-the command :cmd:`Context` to introduce variables into section contexts,
-it works similarly to the :cmd:`Variable` vernacular, except it accepts any
-binding context as argument, so variables can implicit, and
+To ease developments parameterized by many instances, one can use the
+:cmd:`Context` command to introduce these parameters into section contexts,
+it works similarly to the command :cmd:`Variable`, except it accepts any
+binding context as an argument, so variables can be implicit, and
 :ref:`implicit-generalization` can be used.
 For example:
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 398ad4833d..497504e706 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -766,7 +766,7 @@ Sections create local contexts which can be shared across multiple definitions.
 
    Inside a section, local parameters can be introduced using :cmd:`Variable`,
    :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for
-   the former two).
+   the first two).
 
    .. coqtop:: all
 
@@ -827,40 +827,28 @@ Sections create local contexts which can be shared across multiple definitions.
       :name: @ident already exists. (Variable)
       :undocumented:
 
-   .. cmdv:: Variable {+ @ident } : @term
+   .. cmdv:: Variable {+ @ident } : @type
 
       Links :token:`type` to each :token:`ident`.
 
-   .. cmdv:: Variable {+ ( {+ @ident } : @term ) }
+   .. cmdv:: Variable {+ ( {+ @ident } : @type ) }
 
-      Adds blocks of variables with different specifications.
+      Declare one or more variables with various types.
 
-   .. cmdv:: Variables {+ ( {+ @ident } : @term) }
-             Hypothesis {+ ( {+ @ident } : @term) }
-             Hypotheses {+ ( {+ @ident } : @term) }
+   .. cmdv:: Variables {+ ( {+ @ident } : @type) }
+             Hypothesis {+ ( {+ @ident } : @type) }
+             Hypotheses {+ ( {+ @ident } : @type) }
       :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}.
-
-.. seealso:: Section :ref:`contexts` in chapter :ref:`typeclasses`.
+      These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`.
 
 .. cmd:: Let @ident := @term
 
    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 definitions and
-   theorems within the section and depending on :token:`ident` are
-   prefixed by the let-in definition :n:`let @ident := @term in`.
+   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)
@@ -877,6 +865,19 @@ Sections create local contexts which can be shared across multiple definitions.
       :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
 -------------
@@ -2100,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 67e59768d6..e67f53c950 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -636,14 +636,14 @@ has type :token:`type`.
              Hypotheses {+ ( {+ @ident } : @type ) }
       :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section)
 
-      Out of any section, these variants are synonyms of
+      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`.
 
       .. warn:: @ident is declared as a local axiom [local-declaration,scope]
 
-         Warning that is emitted when using :cmd:`Variable` instead of
+         Warning generated when using :cmd:`Variable` instead of
          :cmd:`Local Parameter`.
 
 .. note::
@@ -694,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
@@ -714,14 +714,14 @@ Section :ref:`typing-rules`.
    .. cmdv:: Let @ident := @term
       :name: Let (outside a section)
 
-      Out of any section, this variant is a synonym of
+      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`.
 
       .. warn:: @ident is declared as a local definition [local-declaration,scope]
 
-         Warning that is emitted when using :cmd:`Let` instead of
+         Warning generated when using :cmd:`Let` instead of
          :cmd:`Local Definition`.
 
 .. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`,