| 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 |