This layer adds support for the Proof General interface to the Coq Proof Assistant.
- Loads the company-coq extension
To use this configuration layer,
clone this repository into ~/emacs.d/private/.
You will need to add coq as one of the
dotspacemacs-configuration-layers
in your ~/.spacemacs file.
- Coq (of course)
- Proof general
| Key | Description |
|---|---|
SPC m <dotspacemacs-major-mode-leader-key> | go to this point |
SPC m n | go to next point |
SPC m u | go to previous point |
SPC m h | help at point |
SPC m x | quit Coq |
SPC m ll | Layout: reset |
SPC m lp | Layout: proof |
SPC m s | Search a theorem |
SPC m ? | Check |
SPC m p | |
SPC m ; | insert goal as comment |
SPC m o | occur |
M-k | go to previous point |
M-j | go to next point |
M-l | go to this point |