Coq IDE for vim users -- it is less painful to put up with evil-mode issues than with the issues of any coq plugin for vim

.emacs.el

;; coq
(require 'proof-site "/usr/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")
(setq coq-mode-abbrev-table '())
(add-hook 'coq-mode-hook #'(lambda () (modify-syntax-entry ?_ "w")))
(add-hook 'coq-mode-hook #'(lambda () (modify-syntax-entry ?' "w")))

;; vim-style shortcuts
(require 'undo-tree)
(require 'evil)
  (evil-mode 1)