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 ------------ 1 file changed, 12 deletions(-) (limited to 'coq/coq.el') 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) -- cgit v1.2.3