| 1 | Index: coq/coq.el |
|---|
| 2 | =================================================================== |
|---|
| 3 | RCS file: /disk/cvs/proofgen/ProofGeneral/coq/coq.el,v |
|---|
| 4 | retrieving revision 10.71 |
|---|
| 5 | diff -c -r10.71 coq.el |
|---|
| 6 | *** coq/coq.el 1 Oct 2010 15:52:35 -0000 10.71 |
|---|
| 7 | --- coq/coq.el 1 Oct 2010 20:21:27 -0000 |
|---|
| 8 | *************** |
|---|
| 9 | *** 1167,1172 **** |
|---|
| 10 | --- 1167,1180 ---- |
|---|
| 11 | (substitute-command-keys |
|---|
| 12 | "\\[holes-set-point-next-hole-destroy] to jump to active hole. \\[holes-short-doc] to see holes doc.")))))))))) |
|---|
| 13 | |
|---|
| 14 | + (defun coq-insert-solve-tactic () |
|---|
| 15 | + "Ask for a closing tactic name, with completion on a quasi-exhaustive |
|---|
| 16 | + list of Coq closing tactics, and insert it at point. |
|---|
| 17 | + Questions may be asked to the user." |
|---|
| 18 | + ;; as suggested in trac #357 |
|---|
| 19 | + (interactive) |
|---|
| 20 | + (coq-insert-from-db coq-solve-tactics-db "Closing tactic")) |
|---|
| 21 | + |
|---|
| 22 | (defun coq-insert-tactic () |
|---|
| 23 | "Ask for a tactic name, with completion on a quasi-exhaustive list of coq |
|---|
| 24 | tactics and insert it at point. Questions may be asked to the user." |
|---|
| 25 | *************** |
|---|
| 26 | *** 1201,1206 **** |
|---|
| 27 | --- 1209,1217 ---- |
|---|
| 28 | (define-key coq-keymap [(control ?r)] 'proof-store-response-win) |
|---|
| 29 | (define-key coq-keymap [(control ?G)] 'proof-store-goals-win) |
|---|
| 30 | |
|---|
| 31 | + ;(define-key coq-keymap [(control ?!)] 'coq-insert-solve-tactic) |
|---|
| 32 | + (define-key coq-keymap [?!] 'coq-insert-solve-tactic) ; will work in tty |
|---|
| 33 | + |
|---|
| 34 | (define-key coq-keymap [(control ?\s)] 'coq-insert-term) |
|---|
| 35 | (define-key coq-keymap [(control return)] 'coq-insert-command) |
|---|
| 36 | |
|---|
