coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Christine Paulin <Christine.Paulin AT lri.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: Release of Coq V6.2.1
- Date: Thu, 23 Jul 1998 16:47:15 +0200 (MEST)
The Coq team is pleased to announce the availability of an updated
version of Coq : V6.2.1
6.2.1 is mainly a bug-fix release. Several important bugs have been
corrected, and minor speed improvements (in typing or extraction) were
realized. The changes are :
- Bug-fixes in the Omega and Ring tactics
- more precise syntax of integer expressions. For example
`(Zinv 1)` is printed as is and no more `-1` : this avoid confusion.
(Zinv x) is still printed `-x`.
- Extraction now generates less universes and is more efficient
- the tactic Auto is somewhat faster (Auto in V6.2 was much slower
than in V6.2.beta) .
"Print Hint" has a new meaning : it displays the hints that apply to
the current goal. "Print Hint *" has replaced the old command "Print
Hint" and prints all hints.
- Programs has been much debugged, but it is still in beta-test. It is
now included in the documentation
- "if then else" and "let in" expessions are now printed as they are
parsed - several error messages are now more explicit
- Bug-fixes in unification and in Program
- Printing of tactic scripts is nicer
- "make install" now allowed with do_Makefile
- new commands "Set Printing Depth/Print Printing Depth"
- Improvements of the chapter "Writing you own tactics" of the doc
Main changes between Coq versions V6.1 and V6.2 are described in the
file ftp://ftp.inria.fr/INRIA/Projects/coq/coq/V6.2/doc/Changes.dvi.gz.
The current version can be used with an xemacs interface designed by
the Lego team at Edinburgh University for the Coq and LEGO proof
assistants. It is available from
http://www.dcs.ed.ac.uk/home/lego/html/emacs-2.0.html
A graphic interface for Windows 95 has been written by Gang Chen
http://www.dmi.ens.fr/~gang/
An updated version of the CtCoq interface should be soon available
http://www.inria.fr/croap/ctcoq/ctcoq-eng.html
Coq V6.2.1 is available as source code, binary distribution for linux/Intel,
Solaris/Sparc, Digital Unix/Alpha and Windows NT/95 (soon available).
In case of installation problem, mail to
coq AT pauillac.inria.fr.
There exists a moderated mailing list for general questions or remarks
about Coq: send a mail to
Coq-Club AT pauillac.inria.fr.
Please, use
Coq-Club-request AT pauillac.inria.fr
for [un]subscribing.
--
Christine Paulin-Mohring mailto :
Christine.Paulin AT lri.fr
LRI, URA 410 CNRS, Bat 490, Université Paris Sud, 91405 ORSAY Cedex
LRI tel : (+33) (0)1 69 15 66 35 fax : (+33) (0)1 69 15 65 86
INRIA tel : (+33) (0)1 39 63 55 70 fax : (+33) (0)1 39 63 56 84
Tatoo tel : 06 04 24 44 75
message numerique +1(pas urgent)-3(tres urgent) ou * + message vocal
- Release of Coq V6.2.1, Christine Paulin
Archive powered by MhonArc 2.6.16.