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 <C-backspace>  proof-undo-and-delete-last-successful-command
C-c <C-return>     proof-goto-point
C-c <v>            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 <C-return> coq-insert-command
C-c C-a <C-space>  coq-insert-term