aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2007-04-23 08:59:02 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2007-04-23 08:59:02 +0000
commitda33e3a1fbf241ed3cae9dff44b8aee438a0f60d (patch)
tree4fd002c3ca1effcb7ed5ece06d772e58943d1c16 /coq
parent31e3fe22190e2cb43449beaf5a59fe1c8a58352b (diff)
Fixing bug 110 for SearchRewrite en SearchAbout coq commends.
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 1d75b579..2e887af3 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -674,11 +674,11 @@ This is specific to `coq-mode'."
(defun coq-SearchRewrite ()
(interactive)
- (coq-ask-do "Search Rewrite" "Search Rewrite" nil))
+ (coq-ask-do "Search Rewrite" "SearchRewrite" nil))
(defun coq-SearchAbout ()
(interactive)
- (coq-ask-do "Search About" "Search About" nil))
+ (coq-ask-do "Search About" "SearchAbout" nil))
(defun coq-Print () "Ask for an ident and print the corresponding term."
(interactive)