The Coq mailing list

[Healfdene Goguen <hhg AT dcs.ed.ac.uk>]

Dear Coq users,

As Christine Paulin mentioned in the announcement of Coq V6.2, we in
the LEGO project at Edinburgh have developed an emacs interface for
Coq and LEGO, available at:
        http://www.dcs.ed.ac.uk/home/lego/html/emacs-2.0.html
The mode currently only runs for xemacs (version 19.14 or later), but
we are working on a version that will run under GNU emacs.

The principal feature of this mode is script management, which allows
you to maintain the consistency of your proof buffer with the state of
the proof assistant.  It also includes font-lock, indentation, and
tags for easy access to definitions in the library or in large
developments.

If you picked up a copy of the emacs mode immediately after Christine
sent the message, you probably have a version that is inconsistent
with the latest release of Coq.  If the file proof.el in the package
is earlier than version 1.39 then you should retrieve a new copy.  We
apologize for any inconvenience this may cause.

We still receive bug reports and are continuing to develop the proof
mode.  Please send us any comments you may have, and if you are
interested in new developments check the page on occasion to see when
the release was last updated.

Yours,
Healfdene GOGUEN
Thomas KLEYMANN