From 911a3bf975ddb933acc0f7e17c465005a5ee8465 Mon Sep 17 00:00:00 2001
From: Lysxia
Date: Sat, 16 Mar 2019 20:49:02 -0400
Subject: [Manual] Gather section-specific commands in Section documentation
 (fix #9704)

---
 doc/sphinx/addendum/type-classes.rst | 28 ++++++----------------------
 1 file changed, 6 insertions(+), 22 deletions(-)

(limited to 'doc/sphinx/addendum')

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
 
-- 
cgit v1.2.3