From: Benjamin Werner Subject: web page on automated reasoning -- update To: clt@sail.stanford.edu Date: Fri, 19 Jul 1996 17:31:58 +0200 (MET DST) X-Mailer: ELM [version 2.4 PL24 ME8] MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII Content-Length: 563 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: Benjamin.Werner@inria.fr Phone: +33 (1) 39 63 52 31 Fax: +33 (1) 39 63 53 30 http://pauillac.inria.fr/~werner ----------------------------------------------------------------------------- From: Coq Team Subject: Coq V5.10 Release To: coq-club-redistribution@pauillac.inria.fr, bra-types@cs.chalmers.se, types@dcs.gla.ac.uk, qed@mcs.anl.gov, chet@watson.ibm.com Date: Tue, 4 Jul 1995 15:32:53 +0200 (MET DST) Cc: werner@pauillac.inria.fr (Benjamin Werner) X-Mailer: ELM [version 2.4 PL21] Content-Type: text Content-Length: 1839 Sender: owner-qed@mcs.anl.gov 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 coq@pauillac.inria.fr and general questions to coq-club@pauillac.inria.fr We apologize for possible multiple copies of this message. The Coq team