The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

The Coq team is happy to announce the release of the new version of Coq : V6.2

This version is still in beta test, the final release is scheduled for 
March.

The new features are :
        - faster parsing based on the use of camlp4 for extensible
grammar generation;
        - more uniform syntax for grammar and pretty-print commands;
        - distribution in binary format for some unix systems 
          (linux-pc and solaris-sparc);
        - a version running under windows 95/NT;
        - new tactics and commands to reduce terms or goals;
        - an easier and more direct mechanism to introduce new tactics
        as macros;
        - an experimental tactic called Refine to give incomplete
        terms as proof schema;
        - a command SearchIsos to find a lemma in the libraries from its
        type; 
        - several optimisations and bug fixes in the code.

It is available from
     ftp://ftp.inria.fr/INRIA/Projects/coq/coq/V6.2.beta

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.beta/doc/Changes.dvi.gz.
The Reference Manual for Coq V6.2 is not yet 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