Proof Generalのholes-modeを無効化 - QiitaProof GeneralでCoqファイルを開くと、holes-modeというマイナーモードが立ち上がります。 個人的にはC-c C-jを、カーソルの位置まで証明を進める (proof-goto-point) にバインドしたいのですが、holes-modeのバインドに消されて厄介なので、アドバイスを使ってholes-modeを無効にしてみました。 以下のコードを.emacsに追加するればOKです。 (defadvice coq-mode-config (after deactivate-holes-mode () activate) "Deactivate holes-mode when coq-mode is activated." (progn (holes-mode 0)) )
