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 |