The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

Gabriel Scherer writes:

> I'm not sure what you mean by "debug Ltac", but regarding coq-modes,
> you may consider giving Emacs a try (it is rather easy to use in a
> simple way, and I know some long-time vimers use Emacs just for
> Proof-General). There is also a fairly young project or providing a
> proof-general-like interface for Vim, named "Coquille" (
> https://github.com/trefis/coquille ). It's in an early stage of
> development, but you may give it a try.

To keep using vim key bindings with emacs, you may consider evil
(http://www.emacswiki.org/emacs/Evil). I know several vimers who use it
when they run proof general.

Alan