Add a new binding for the Coq layer.

This binding toggles the electric terminator setting of Proof General.

Also describe the new binding in the README and add a note to the change
log.
This commit is contained in:
Ignat Insarov 2020-02-11 23:46:39 +03:00 committed by Maximilian Wolff
parent 30250403a2
commit d44522ee1d
No known key found for this signature in database
GPG Key ID: 2DD07025BFDBD89A
3 changed files with 12 additions and 1 deletions

View File

@ -1569,6 +1569,9 @@ Other:
- Fixed ~SPC m e~ key bindings to behave like in Emacs Lisp
(thanks to Boris Avdeev)
- Fixed initialization of =counsel-gtags= (thanks to Sylvain Benner)
**** Coq
- Key bindings:
- ~SPC m T e~ Toggle electric terminator (thanks to Ignat Insarov)
**** Cscope
- Key bindings:
- Fixed key binding ~g C~ (thanks to dubnde)

View File

@ -127,3 +127,9 @@ 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
available =company-coq= key bindings can be accessed at any time using =SPC SPC
company-coq-tutorial=.
** Options
| Key binding | Description |
|-----------------+-----------------------------|
| ~SPC m T e~ | Toggle electric terminator. |

View File

@ -104,7 +104,9 @@
"ir" 'coq-insert-requires
"is" 'coq-insert-section-or-module
"it" 'coq-insert-tactic
"iT" 'coq-insert-tactical))))
"iT" 'coq-insert-tactical
;; Options
"Te" 'proof-electric-terminator-toggle))))
(defun coq/post-init-smartparens ()
(spacemacs/add-to-hooks (if dotspacemacs-smartparens-strict-mode