Coq-modeでj,kで証明を進めたい場合

gistfile1.el

;;; M-x coq-vi-modeでマイナーモードとして使ってください
(define-minor-mode coq-vi-mode
  "Vi like proof in Proof General"
  :lighter "coq-vi"
  :keymap (let ((map (make-sparse-keymap)))
            (define-key map "j" 'proof-assert-next-command-interactive) ;C-c C-n
            (define-key map "k" 'proof-undo-last-successful-command) ;C-c C-u
            map)
 )