Proof Generalのholes-modeを無効化

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)))