replug removal of induction principle in SearAbout queries.

1 files changed, 7 insertions, 2 deletions

diff --git a/coq/coq.el b/coq/coq.el
index ff432251..3b716ad0 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -873,8 +873,13 @@ More precisely it executes SETCMD, then DO id and finally silently UNSETCMD."
       (concat "\"" s "\"")
     s))
 
+(defsubst coq-put-into-double-quote-if-notation-remove-ind (s)
+  (if (equal (char-syntax (string-to-char s)) ?\.)
+      (concat "\"" s "\" " "-\"_ind\" - \"_rect\" -\"_rec\"")
+    s))
+
 (defsubst coq-put-into-brackets-remove-useless (s)
-  (concat "[ " s " -\"_ind\" - \"_rect\" -\"_rec\" ]"))
+  (concat s " -\"_ind\" - \"_rect\" -\"_rec\""))
 
 (defsubst coq-put-into-quotes (s)
   (concat "\"" s "\""))
@@ -900,7 +905,7 @@ This is specific to `coq-mode'."
   (interactive)
   (coq-ask-do
    "SearchAbout (ex: \"eq_\" eq -bool)"
-   "SearchAbout" nil 'coq-put-into-double-quote-if-notation)
+   "SearchAbout" nil 'coq-put-into-double-quote-if-notation-remove-ind)
   (message "use `coq-SearchAbout-all' to see constants ending with \"_ind\", \"_rec\", etc"))
 
 (defun coq-SearchAbout-all ()