SearchAbout is deprecated since 8.5; use Search instead

5 files changed, 12 insertions, 23 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 391b1238..d1cb249d 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -261,10 +261,8 @@
      ["About..." coq-About :help "With prefix arg (C-u): Set Printing All first"]
      ["About...(show implicits)" coq-About-with-implicits t]
      ["About...(show all)" coq-About-with-all t]
-     ["Search..." coq-SearchConstant t]
+     ["Search..." coq-Search t]
      ["SearchRewrite..." coq-SearchRewrite t]
-     ["SearchAbout (hiding principles)..." coq-SearchAbout t]
-     ["SearchAbout..." coq-SearchAbout-all t]
      ["SearchPattern..." coq-SearchIsos t]
      ["Locate constant..." coq-LocateConstant t]
      ["Locate Library..." coq-LocateLibrary t]
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 93db1a77..55a12117 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -563,7 +563,6 @@ so for the following reasons:
      ("Print" "p" "Print #." nil "Print")
      ("Pwd" nil "Pwd." nil "Pwd")
      ("Search" nil "Search #" nil "Search")
-     ("SearchAbout" nil "SearchAbout #" nil "SearchAbout")
      ("SearchPattern" nil "SearchPattern (#)" nil "SearchPattern")
      ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite")
      ("Show" nil "Show #." nil "Show")
diff --git a/coq/coq.el b/coq/coq.el
index 8acc1b72..0c934a9b 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1005,17 +1005,10 @@ This is specific to `coq-mode'."
    "SearchPattern (parenthesis mandatory), ex: (?X1 + _ = _ + ?X1)"
    "SearchPattern" nil))
 
-(defun coq-SearchConstant ()
-  (interactive)
-  (coq-ask-do "Search constant" "Search"))
-
 (defun coq-SearchRewrite ()
   (interactive)
   (coq-ask-do "SearchRewrite" "SearchRewrite" nil))
 
-
-
-
 (defun coq-Print (withprintingall)
   "Ask for an ident and print the corresponding term.
 With flag Printing All if some prefix arg is given (C-u)."
@@ -1487,7 +1480,7 @@ fold/unfold cross.  Return the list of mappings hypname -> overlays."
 ;; Feature: highlighting of hypothesis that remains when the script is played
 ;; (and goals buffer is updated).
 
-;; On by default. This only works with the SearchAbout function for now.
+;; On by default. This only works with the Search function for now.
 (defvar coq-highlight-hyps-cited-in-response t
   "If non-nil, try to highlight in goals buffers hyps cited in response.")
 
@@ -1559,7 +1552,7 @@ of hypothesis to highlight."
 
 (defun coq-get-hyps-cited-in-response ()
   "Returns locations of hyps in goals buffer that are cited in response buffer.
-See `coq-highlight-hyps-cited-in-response' and `SearchAbout'."
+See `coq-highlight-hyps-cited-in-response' and `Search'."
   (let* ((hyps-cited-pos (coq-detect-hyps-positions proof-response-buffer))
          (hyps-cited (coq-build-hyps-names hyps-cited-pos)))
     (cl-remove-if-not
@@ -2678,15 +2671,13 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
          "Set Printing All" q "Unset Printing All" nil "Test Printing All")
       (proof-shell-invisible-command q))))
 
-
-;; TODO SearchAbout become Search in v8.5, change when V8.4 becomes old.
-(defun coq-SearchAbout ()
+(defun coq-Search ()
   (interactive)
   (coq-ask-do
    ;; TODO: use [Add Search Blacklist "foo"] to exclude optionaly some patterns:
    ;;  "_ind" "_rec" "R_" "_equation"
-   "SearchAbout (ex: \"eq_\" eq -bool)"
-   "SearchAbout"
+   "Search (ex: \"eq_\" eq -bool)"
+   "Search"
    nil nil t)
   (when coq-highlight-hyps-cited-in-response
     (coq-highlight-hyps-cited-in-response)
@@ -2694,6 +2685,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
   (unless coq-highlight-hyps-cited-in-response
     (message "[Coq/Settings/Search Blacklist] to change blacklisting.")))
 
+
 ;; Insertion commands
 (define-key coq-keymap [(control ?i)] 'coq-insert-intros)
 (define-key coq-keymap [(control ?m)] 'coq-insert-match)
@@ -2717,7 +2709,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
 (define-key coq-keymap [(control ?o)] 'coq-SearchIsos)
 (define-key coq-keymap [(control ?p)] 'coq-Print)
 (define-key coq-keymap [(control ?b)] 'coq-About)
-(define-key coq-keymap [(control ?a)] 'coq-SearchAbout)
+(define-key coq-keymap [(control ?a)] 'coq-Search)
 (define-key coq-keymap [(control ?c)] 'coq-Check)
 (define-key coq-keymap [?h] 'coq-PrintHint)
 (define-key coq-keymap [(control ?l)] 'coq-LocateConstant)
@@ -2734,7 +2726,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
 (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?p)] 'coq-Print)
 (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?o)] 'coq-SearchIsos)
 (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?b)] 'coq-About)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?a)] 'coq-SearchAbout)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?a)] 'coq-Search)
 (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?s)] 'coq-Show)
 (define-key coq-goals-mode-map [(control ?c)(control ?a)?r] 'proof-store-response-win)
 (define-key coq-goals-mode-map [(control ?c)(control ?a)?g] 'proof-store-goals-win)
@@ -2754,7 +2746,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
 (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?p)] 'coq-Print)
 (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?o)] 'coq-SearchIsos)
 (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?b)] 'coq-About)
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?a)] 'coq-SearchAbout)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?a)] 'coq-Search)
 (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?s)] 'coq-Show)
 (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?r)] 'proof-store-response-win)
 (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?g)] 'proof-store-goals-win)
diff --git a/coq/faq b/coq/faq
index 40873850..8b2cb06f 100644
--- a/coq/faq
+++ b/coq/faq
@@ -113,7 +113,7 @@ printing options temporarily disable (Set Printing All).
 
 *** C-c C-a C-p The same for a ``Print '' query.
 *** C-c C-a C-b The same for a ``About '' query.
-*** C-c C-a C-a The same for a ``SearchAbout '' query (no C-u prefix).
+*** C-c C-a C-a The same for a ``Search '' query (no C-u prefix).
 *** C-c C-a C-o The same for a Search ``SearchIsos'' (no C-u prefix).
 
 ** I hate menus, why do you have menus?
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 23aba63b..699b304b 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4342,7 +4342,7 @@ The same for a ``Print '' query.
 @item C-c C-a C-b
 The same for a ``About '' query.
 @item C-c C-a C-a
-The same for a ``SearchAbout '' query (no C-u prefix).
+The same for a ``Search '' query (no C-u prefix).
 @item C-c C-a C-o
 The same for a Search ``SearchIsos'' (no C-u prefix).