TakeV
/
spacemacs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lang/coq: more insertion keybindings

This commit is contained in:
Langston Barrett 2018-08-02 17:24:54 -07:00 committed by Codruț Constantin Gușoi
parent 6058921a02
commit 178b0caeb8
2 changed files with 13 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
layers/+lang/coq/README.org
View File

@ -102,9 +102,15 @@ The mnemonic for =a= is "ask".
|-----------------+-----------------------------------------------------------------|
| ~SPC m M-RET~ | Insert regular match branch |
| ~SPC m M-S-RET~ | Insert =match goal with= branch |
| ~SPC m i c~ | Insert a vernacular command |
| ~SPC m i e~ | Insert =End <section-name>= |
| ~SPC m i i~ | Insert =intros= with default variable names |
| ~SPC m i l~ | Extract lemma from current goal - exit with ~C-RET~ (not ~C-j~) |
| ~SPC m i m~ | Insert =match= on a type |
| ~SPC m i r~ | Insert a =Require= statement |
| ~SPC m i s~ | Insert a =Section= or =Module= |
| ~SPC m i t~ | Insert a tactic |
| ~SPC m i T~ | Insert a tactical |
Note the last two are regular =company-coq= bindings, left alone since they are
most useful in insert mode. The full =company-coq= tutorial showcasing all

8
layers/+lang/coq/packages.el
View File

@ -95,7 +95,13 @@
"gl" 'proof-goto-end-of-locked
"gs" 'proof-goto-command-start
;; Insertions
"ie" 'coq-end-Section))))
"ic" 'coq-insert-command
"ie" 'coq-end-Section
"ii" 'coq-insert-intros
"ir" 'coq-insert-requires
"is" 'coq-insert-section-or-module
"it" 'coq-insert-tactic
"iT" 'coq-insert-tactical))))
(defun coq/post-init-smartparens ()
(spacemacs/add-to-hooks (if dotspacemacs-smartparens-strict-mode