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 --- .../07-commands-and-options/11944-rm-searchabout-cmd.rst | 3 +++ doc/sphinx/proof-engine/vernacular-commands.rst | 12 ------------ doc/tools/docgram/common.edit_mlg | 4 ---- doc/tools/docgram/fullGrammar | 4 ---- doc/tools/docgram/orderedGrammar | 4 ---- 5 files changed, 3 insertions(+), 24 deletions(-) create mode 100644 doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst (limited to 'doc') 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 `_, 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: [ -- cgit v1.2.3