diff options
author | 1999-10-06 10:53:06 +0000 | |
---|---|---|
committer | 1999-10-06 10:53:06 +0000 | |
commit | aa272b4524fd7510fc9ddbe8142e408318238301 (patch) | |
tree | 3fdc360c3478663cc5720ec6a3af6f77ab467516 /coq/coq.el | |
parent | e0706d87ee5550e452c964fffb240aa74a2aa9b7 (diff) |
Remove coq-Search function, now generic.
Diffstat (limited to 'coq/coq.el')
-rw-r--r-- | coq/coq.el | 12 |
1 files changed, 0 insertions, 12 deletions
@@ -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) |