Subject: web page on automated reasoning -- update
From: Benjamin Werner <[email-masked]>
To: [email-masked]
Date: Fri, 19 Jul 1996 17:31:58 +0200 (MET DST)

Dear Carolyn,

You might want to update the pointer to Coq (proof checker) in your
page. The correct link is:

http://pauillac.inria.fr/coq/systeme_coq-eng.html

Thanks a lot.

Cheers,

Benjamin Werner
----------------------------------------------------------------------------
Projet Coq
INRIA-Rocquencourt, BP 105, F-78 153 LE CHESNAY cedex, FRANCE
E-mail: [email-masked]
Phone: +33 (1) 39 63 52 31
Fax:   +33 (1) 39 63 53 30
http://pauillac.inria.fr/~werner
-----------------------------------------------------------------------------

From: Coq Team <[email-masked]>
Subject: Coq V5.10 Release
To: [email-masked], [email-masked],
        [email-masked], [email-masked], [email-masked]
Date: Tue, 4 Jul 1995 15:32:53 +0200 (MET DST)
Cc: [email-masked] (Benjamin Werner)
X-Mailer: ELM [version 2.4 PL21]
Content-Type: text
Content-Length: 1839      
Sender: [email-masked]
Precedence: bulk

                  Coq V5.10 Release

This is the announcement for the release of the Coq Proof Assistant,
Version 5.10.

It may be taken as usual from machine ftp.inria.fr, directory
INRIA/coq/V5.10, archive V5.10.tar.z and README file.

For users who are already using one of the beta-test versions of V5.10,
this final release has improved documentation, streamlining of tactics
(Some adaptation of your scripts may be necessary because the names
of inversion tactics have changed), and compressed theory files (.vo)
which keep the size of the installation much smaller and are uniform
across architectures. This substantial improvement necessitates
however the installation of the latest release of Caml Light; see
WARNING below. 

For users who are still using our old release V5.8, it is high time to
switch to this new system, which has been completely rebuilt, 
authorizes mutually recursive inductive families, compiled theory
modules, extensible parsers and pretty-printers, user-programmable
tactics, synthesis of implicit type arguments, and many other goodies.
The distribution also includes numerous new user-contributed
libraries. 

The current release works under most modern UNIX platforms.
A specialised interface with the Centaur environment, called CTCoq, is
under completion in Sophia-Antipolis and should be available soon
in beta-test. 

A Macintosh version will be available next Fall.

* WARNING: In order to install Coq V5.10 you NEED to install the latest
* release of Caml Light 0.7, available by anonymous ftp on
* ftp.inria.fr, in INRIA/lang/caml-light. You also need to
* install the Caml Light contribution `libunix'.

As always, anomaly reports to [email-masked]
and general questions to [email-masked]

We apologize for possible multiple copies of this message.

  The Coq team