Remove SearchAbout command, deprecated in 8.5

5 files changed, 3 insertions, 24 deletions

diff --git a/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst
new file mode 100644
index 0000000000..e409c638bb
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst
@@ -0,0 +1,3 @@
+- **Removed:** Removed SearchAbout command that was deprecated in 8.5.
+  Use :cmd:`Search` instead.
+  (`#11944 <https://github.com/coq/coq/pull/11944>`_, by Jim Fehrle).
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
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 88a5217652..60b845c4be 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1125,10 +1125,6 @@ query_command: [
 | WITH "SearchRewrite" constr_pattern in_or_out_modules
 | REPLACE "Search" searchabout_query searchabout_queries "."
 | WITH "Search" searchabout_query searchabout_queries
-| REPLACE "SearchAbout" searchabout_query searchabout_queries "."
-| WITH "SearchAbout" searchabout_query searchabout_queries
-| REPLACE "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
-| WITH "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules
 ]
 
 vernac_toplevel: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 241cf48cf1..272d17bb35 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1244,8 +1244,6 @@ query_command: [
 | "SearchPattern" constr_pattern in_or_out_modules "."
 | "SearchRewrite" constr_pattern in_or_out_modules "."
 | "Search" searchabout_query searchabout_queries "."
-| "SearchAbout" searchabout_query searchabout_queries "."
-| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
 ]
 
 printable: [
@@ -2454,8 +2452,6 @@ as_or_and_ipat: [
 
 eqn_ipat: [
 | "eqn" ":" naming_intropattern
-| "_eqn" ":" naming_intropattern
-| "_eqn"
 |
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 38e7b781df..0c9d7a853b 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -918,8 +918,6 @@ command: [
 | "SearchPattern" one_term OPT ne_in_or_out_modules
 | "SearchRewrite" one_term OPT ne_in_or_out_modules
 | "Search" searchabout_query OPT searchabout_queries
-| "SearchAbout" searchabout_query OPT searchabout_queries
-| "SearchAbout" "[" LIST1 searchabout_query "]" OPT ne_in_or_out_modules
 | "Time" command
 | "Redirect" string command
 | "Timeout" num command
@@ -1441,8 +1439,6 @@ as_or_and_ipat: [
 
 eqn_ipat: [
 | "eqn" ":" naming_intropattern
-| "_eqn" ":" naming_intropattern
-| "_eqn"
 ]
 
 as_name: [