From 88c702dfac4adb8bf590a2bdf30e76c7c6cb892f Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 29 Apr 2018 00:38:54 +0200
Subject: [sphinx] Fix new warnings related to tacn, cmd, opt...

---
 doc/sphinx/user-extensions/proof-schemes.rst     | 1 +
 doc/sphinx/user-extensions/syntax-extensions.rst | 5 ++---
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx/user-extensions')

diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index e12e4d897a..682553c31b 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -26,6 +26,7 @@ induction for objects in type `identᵢ`.
   natural in case of inductively defined relations.
 
 .. cmdv:: Scheme Equality for @ident
+   :name: Scheme Equality
 
    Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident`
    involves some other inductive types, their equality has to be defined first.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 6958b5f265..3b95a37ed3 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -916,9 +916,8 @@ Binding arguments of a constant to an interpretation scope
 
 .. seealso::
 
-   :cmd:`About @qualid`
-     The command to show the scopes bound to the arguments of a
-     function is described in Section 2.
+   The command :cmd:`About` can be used to show the scopes bound to the
+   arguments of a function.
 
 .. note::
 
-- 
cgit v1.2.3