From aa272b4524fd7510fc9ddbe8142e408318238301 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 6 Oct 1999 10:53:06 +0000
Subject: Remove coq-Search function, now generic.

---
 coq/coq.el    | 12 ------------
 coq/example.v |  2 ++
 2 files changed, 2 insertions(+), 12 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index c84b9719..ef3f5a8d 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -289,17 +289,6 @@
     (proof-shell-invisible-command
      (concat "SearchIsos " cmd proof-terminal-string))))
 
-(defun coq-Search ()
-  "Search all constant that have the given head symbol
-
-  This is specific to coq-mode."
-  (interactive)
-  (let (cmd)
-    (proof-shell-ready-prover) 
-    (setq cmd (read-string "Search: " nil 'proof-minibuffer-history))
-    (proof-shell-invisible-command
-     (concat "Search " cmd proof-terminal-string))))
-
 (defun coq-begin-Section ()
   "begins a Coq section."
   (interactive)
@@ -457,7 +446,6 @@
 
   (define-key (current-local-map) [(control c) ?I] 'coq-Intros)
   (define-key (current-local-map) [(control c) ?a] 'coq-Apply)
-  (define-key (current-local-map) [(control c) (control s)] 'coq-Search)
   (define-key (current-local-map) [(control c) ?s] 'coq-begin-Section)
   (define-key (current-local-map) [(control c) ?e] 'coq-end-Section)
   (define-key (current-local-map) [(control c) (control m)] 'coq-Compile)
diff --git a/coq/example.v b/coq/example.v
index 619072c2..4fb38af6 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -11,3 +11,5 @@ Apply conj.
 Assumption.
 Assumption.
 Save and_comms.
+
+
-- 
cgit v1.2.3