diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-10-06 10:53:06 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-10-06 10:53:06 +0000 |
| commit | aa272b4524fd7510fc9ddbe8142e408318238301 (patch) | |
| tree | 3fdc360c3478663cc5720ec6a3af6f77ab467516 /coq | |
| parent | e0706d87ee5550e452c964fffb240aa74a2aa9b7 (diff) | |
Remove coq-Search function, now generic.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq.el | 12 | ||||
| -rw-r--r-- | coq/example.v | 2 |
2 files changed, 2 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) 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. + + |