The Coq mailing list

[Christine Paulin <paulin AT lri.fr>]

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

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, solaris-sparc and digital-alpha);
        - new tactics and commands to reduce terms or goals;
        - an easier and more direct mechanism to introduce new tactics
        as macros;
        - a command SearchIsos to find a lemma in the libraries from its
        type; 
        - a few new tactics 
                - tactics for decomposing hypothesis in inductive definitions;
                - an experimental tactic called Refine to give incomplete
        terms as proof schema;
                - a tactical Abstract to save an intermediate goal as a 
theorem
                - extension of the Intros tactic to give names to
components of an hypothesis.
        - several optimisations and bug fixes in the code.
        - a version running under windows 95/NT is coming soon

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

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 Reference Manual for Coq V6.2 has been updated and reorganised,
the chapters concerning syntactic extensions and customized
tactics have been completely rewritten. The documentation is also 
available in html format. Both versions of the documentation are still
in draft format.  

The current version can be used with an emacs 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

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.

                The Coq team
-- 
  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