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.