ProofGeneral/Keybinds

Key Binding
C-c C-b proof-process-buffer
C-c C-c proof-interrupt-process
C-c C-f proof-find-theorems
C-c C-h proof-help
C-c C-l proof-layout-windows
C-c C-n proof-assert-next-command-interactive
C-c C-o proof-display-some-buffers
C-c C-p proof-prf
C-c C-r proof-retract-buffer
C-c C-s proof-shell-start
C-c C-t proof-ctxt
C-c C-u proof-undo-last-successful-command
C-c C-v proof-minibuffer-cmd
C-c C-w pg-response-clear-displays
C-c C-x proof-shell-exit
C-c C-z proof-frob-locked-end
C-c . proof-electric-terminator-toggle
C-c ` proof-next-error
C-c C-. proof-goto-end-of-locked
C-c C-; pg-insert-last-output-as-comment
C-c proof-undo-and-delete-last-successful-command
C-c proof-goto-point
C-c pg-toggle-visibility
C-c C-a C-b coq-About
C-c C-a C-c coq-Check
C-c C-a C-h coq-PrintHint
C-c C-a TAB coq-insert-intros
C-c C-a C-l coq-LocateConstant
C-c C-a RET coq-insert-match
C-c C-a C-n coq-LocateNotation
C-c C-a C-o coq-SearchIsos
C-c C-a C-p coq-Print
C-c C-a C-r coq-insert-requires
C-c C-a C-s coq-Show
C-c C-a C-t coq-insert-tactic
C-c C-a C-S-t coq-insert-tactical
C-c C-a C-( coq-insert-section-or-module
C-c C-a C-) coq-end-Section
C-c C-a coq-insert-command
C-c C-a coq-insert-term