From 3bd1b0b9301322f89057deb9eccd746b075b1694 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <courtieu@lri.fr>
Date: Tue, 9 Dec 2014 10:50:00 +0000
Subject: Added a variant of searchAbout hiding some spurious entries.

---
 coq/coq-abbrev.el | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'coq/coq-abbrev.el')

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 2dcead62..2ccf5cab 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -154,7 +154,8 @@
      ["About...(show all)" coq-About-with-all t]
      ["Search..." coq-SearchConstant t]
      ["SearchRewrite..." coq-SearchRewrite t]
-     ["SearchAbout..." coq-SearchAbout 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]
-- 
cgit v1.2.3