CSC535: Using ProofGeneral [2010/09/05]

There are only a few commands you need to know to use ProofGeneral effectively. They are:
- C-h t: Emacs tutorial.
- C-c C-n: send the next command to Coq.
- C-c C-u: undo (retract) the most recently executed command.
- C-c C-RET: submit everything up to the current cursor location to Coq for processing.
- C-c C-. : move the cursor to the end of the last command which has been processed by Coq.
- C-c . : toggle "electric terminator mode". When this mode is turned on, simply typing a period will send the current command to Coq (normally you have to type a period and then type C-c C-n).
- M-/ : complete the word at the cursor. Hit repeatedly to cycle though options.

I have the following in my emacs initialization file:

;;------------------
;; Proof General
;;------------------
(load-file (expand-file-name "$HOME/Library/packages/ProofGeneral/generic/proof-site.el"))
(eval-after-load "proof-script" '(progn
 ;; these match CoqIDE
 (define-key proof-mode-map [(control meta down)] 'proof-assert-next-command-interactive) ;; C-c C-n
 (define-key proof-mode-map [(control meta up)] 'proof-undo-last-successful-command) ;; C-c C-u
 (define-key proof-mode-map [(control meta right)] 'proof-goto-point) ;; C-c return
 ;; some additional bindings
 (define-key proof-mode-map [(control meta return)] 'proof-goto-point) ;; C-c return
 (define-key proof-mode-map [(control meta .)] 'proof-goto-end-of-locked) ;; C-c C-.
 (define-key proof-mode-map (kbd "C-c C-3") 'proof-three-window-toggle) 
))