Merge PR #7252: Sphinx doc fix warnings

1 files changed, 5 insertions, 6 deletions

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 5518da9acc..8861cac8af 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
 
@@ -333,7 +332,7 @@ Variants:
 
 .. cmd:: Program Instance
 
-   Switches the type-checking to Program (chapter :ref:`program`) and
+   Switches the type-checking to Program (chapter :ref:`programs`) and
    uses the obligation mechanism to manage missing fields.
 
 .. cmd:: Declare Instance