coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ProofGeneral dev release + coq-7.4 -- Announcement --

From: Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr>
To: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>, David Aspinall <da AT dcs.ed.ac.uk>
Subject: [Coq-Club] ProofGeneral dev release + coq-7.4 -- Announcement --
Date: Tue, 11 Feb 2003 14:46:30 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

The new ProofGeneral development release
(http://www.proofgeneral.org/devel) is compatible with coq-7.4 (+ some
bug fixes).

Please recall that since PG-3.4, backtracking of sections (and now
modules) is improved, and that the synchronization mechanism for user
defined commands/tactics is *configurable* via four lisp variables:

coq-user-state-changing-commands
coq-user-state-preserving-commands
coq-user-state-changing-tactics
coq-user-state-preserving-tactics

These variables (regexp lists) can be set in your .emacs file, see their
documentation (ex: C-h v coq-user-state-preserving-tactics), or the
documentation of ProofGeneral.

Bug Reports and remarks are welcome,

Pierre Courtieu

[Coq-Club] ProofGeneral dev release + coq-7.4 -- Announcement --, Pierre Courtieu