The Coq mailing list

[Christine Paulin <paulin AT lri.fr>]

The Coq team is pleased to announce the availability of the new version 
of Coq : V6.3
Warning : this version contains experimental features which are likely 
to be modified soon, a more robust distribution is planned for september.
However, we encourage you to test this version and send us anomaly reports. 

Changes from V6.2.4 are mainly the addition of new features
===========================================================

  - Change in the guard condition for fixpoint definition 
which allows more functions to be defined on nested
inductive definitions (Inductive term : Set := cons : (list term)->term)
  - A new (still very experimental) tactic AutoRewrite to apply 
successively a set of rewriting lemmas
  - A new tactic Quote to generate automatically the inverse image 
of a term by an interpretation function 
  - Timing of Coq commands
  - Reducing a term before defining it
  - Focus on a specific goal
  - Extension of tactics Induction, Intro
  - Extension of the algorithm for type inference
  - ...

Look at the file CHANGES in the distribution or 
        http://coq.inria.fr/doc/changes.html
for more information on the changes.

Coq V6.3 is available as source code, binary distribution for
Linux/Intel, Solaris/Sparc, Digital Unix/Alpha and
Windows NT/95/98. 
Coq V6.3 can be obtained, and the documentation too, directly at

  ftp://ftp.inria.fr/INRIA/coq/V6.3

or via http://coq.inria.fr

The graphic interface CtCoq provides a working environment for 
the Coq theorem prover (to get
it, see http://www.inria.fr/croap/ctcoq/ctcoq-eng.html).

There is also a powerful emacs mode for Coq called Proof General
(see http://www.dcs.ed.ac.uk/home/proofgen).

A graphic interface for Windows 95 has been written by Gang Chen
http://www.dmi.ens.fr/~gang/

Installation problems:        mail to 
coq AT pauillac.inria.fr.
General questions or remarks: mail to 
Coq-Club AT pauillac.inria.fr
 (moderated)
Subscribing/unsubscribing:    mail to 
Coq-Club-request AT pauillac.inria.fr

-- 
  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 54 60       fax : (+33) (0)1 39 63 56 84
  Tatoo tel : 06 04 24 44 75