12.7 Coq and GNU Emacs

Coq comes with a Major mode for GNU Emacs, coq.el. This mode provides syntax highlighting (assuming your GNU Emacs library provides hilit19.el) and also a rudimentary indentation facility in the style of the Caml GNU Emacs mode.

Add the following lines to your .emacs file:

  (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
  (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)

The Coq major mode is triggered by visiting a file with extension .v, or manually with the command M-x coq-mode. It gives you the correct syntax table for the Coq language, and also a rudimentary indentation facility:

pressing Tab at the beginning of a line indents the line like the line above;
extra Tabs increase the indentation level (by 2 spaces by default);
M-Tab decreases the indentation level.