From 2a803690d76724fd7c97288f208f3a1faf98eca1 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Fri, 27 Mar 2020 21:55:37 -0700
Subject: Remove SearchAbout command, deprecated in 8.5

---
 doc/sphinx/proof-engine/vernacular-commands.rst | 12 ------------
 1 file changed, 12 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 c33d62532e..c6a3697916 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -321,18 +321,6 @@ Requests to the environment
 
             Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
 
-   .. cmdv:: SearchAbout
-      :name: SearchAbout
-
-      .. deprecated:: 8.5
-
-      Up to |Coq| version 8.4, :cmd:`Search` had the behavior of current
-      :cmd:`SearchHead` and the behavior of current :cmd:`Search` was obtained with
-      command :cmd:`SearchAbout`. For compatibility, the deprecated name
-      :cmd:`SearchAbout` can still be used as a synonym of :cmd:`Search`. For
-      compatibility, the list of objects to search when using :cmd:`SearchAbout`
-      may also be enclosed by optional ``[ ]`` delimiters.
-
 
 .. cmd:: SearchHead @term
 
-- 
cgit v1.2.3