diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-14 21:57:53 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-14 21:59:15 +0200 |
| commit | ab2e6772c6cbe2e6fa8851a1b399222a2a7740e3 (patch) | |
| tree | 8bd8a4bd811af8a57f7b675741221a5a9c849511 /doc/sphinx/addendum/type-classes.rst | |
| parent | 3cc6a433d025996ea4a61969517d45ffbc9fd8a9 (diff) | |
[Sphinx] Fix all remaining warnings.
Diffstat (limited to 'doc/sphinx/addendum/type-classes.rst')
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index add03b946..8861cac8a 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -148,11 +148,10 @@ database. Sections and contexts --------------------- -To ease the parametrization of developments by type classes, we -provide a new way to introduce variables into section contexts, -compatible with the implicit argument mechanism. The new command works -similarly to the ``Variables`` vernacular (:ref:`TODO-1.3.2-Definitions`), except it -accepts any binding context as argument. For example: +To ease the parametrization of developments by type classes, 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: .. coqtop:: all |