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

1 files changed, 6 insertions, 22 deletions

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index a463a73bef..8e6f85fca3 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -146,10 +146,12 @@ database.
 Sections and contexts
 ---------------------
 
-To ease the parametrization of developments by typeclasses, we provide a new
-way to introduce variables into section contexts, compatible with the implicit
-argument mechanism. The new command works similarly to the :cmd:`Variables`
-vernacular, except it accepts any binding context as argument. For example:
+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
+:ref:`implicit-generalization` can be used (see also :ref:`section-mechanism`).
+For example:
 
 .. coqtop:: all
 
@@ -358,24 +360,6 @@ few other commands related to typeclasses.
    equivalent to ``Hint Resolve ident : typeclass_instances``, except it
    registers instances for :cmd:`Print Instances`.
 
-.. 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::
-
-       Section ContextExample.
-
-       Context {A : Type} (a b : A).
-       Context `{EqDec A}.
-
-       (* ... *)
-
-       End ContextExample.
-
-   See also :ref:`contexts`.
-
 .. tacn:: typeclasses eauto
    :name: typeclasses eauto