More than 5 years have passed since last update.
Proof GeneralでCoqファイルを開くと、holes-modeというマイナーモードが立ち上がります。
個人的にはC-c C-jを、カーソルの位置まで証明を進める (proof-goto-point) にバインドしたいのですが、holes-modeのバインドに消されて厄介なので、アドバイスを使ってholes-modeを無効にしてみました。
以下のコードを.emacsに追加するればOKです。
.emacs
(defadvice coq-mode-config (after deactivate-holes-mode () activate)
"Deactivate holes-mode when coq-mode is activated."
(progn (holes-mode 0))
)
なお、C-c C-jを (proof-goto-point) にバインドするコードは、例えば以下のような感じです。
.emacs
(add-hook 'proof-mode-hook
'(lambda ()
(define-key proof-mode-map (kbd "C-c C-j") 'proof-goto-point)))
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme