coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] New development release of ProofGeneral

From: Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>
To: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] New development release of ProofGeneral
Date: Wed, 24 Mar 2004 15:39:53 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

A new development release of ProofGeneral is available at

http://zermelo.dcs.ed.ac.uk/develdownload.html

New features for coq:

- Indentation;

- Menus for commands and tactics, including a system of "holes" allowing
to quickly fill complex expressions.

Bugs:

- PG is not yet adapted to work with the latest version of X-Symbols.

It is adapted to coq v8, bug reports are welcome
(Pierre.Courtieu AT univ-orleans.fr)

Cheers,

Pierre Courtieu

[Coq-Club] New development release of ProofGeneral, Pierre Courtieu