From b6f3e7696ec73cb919343d54dcfe9f62a787be54 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 5 Nov 2020 12:32:39 +0100
Subject: Various fixes.

---
 doc/sphinx/proof-engine/vernacular-commands.rst | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 301559d69d..dd0b12f8ec 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -990,11 +990,6 @@ described first.
    has to check the conversion (see Section :ref:`conversion-rules`) of two distinct
    applied constants.
 
-   .. seealso::
-
-      Sections :ref:`performingcomputations`, :ref:`tactics-automating`,
-      :ref:`proof-editing-mode`
-
 .. cmd:: Transparent {+ @reference }
 
    This command accepts the :attr:`global` attribute.  By default, the scope
@@ -1015,10 +1010,7 @@ described first.
 
       There is no constant named :n:`@qualid` in the environment.
 
-      .. seealso::
-
-         Sections :ref:`performingcomputations`,
-         :ref:`tactics-automating`, :ref:`proof-editing-mode`
+.. seealso:: :ref:`performingcomputations` and :ref:`proof-editing-mode`
 
 .. _vernac-strategy:
 
-- 
cgit v1.2.3