The Coq mailing list

[Patrick Loiseleur <Patrick.Loiseleur AT lri.fr>]

The Coq team is pleased to announce the availability of an updated 
version of Coq : V6.2.3

6.2.3 is both a maintenance release and a next step in the way of proof
automation. The main change is the reorganization of the Hints for Auto
in fonctionnal databases, that gives to the user more control on what to
use and what not to use as a hint for Auto. To do this change and to get
ready to add new features, the syntax of the "Hint" command has changed.
Thus the syntax of V6.2.3 is not compatible with V6.2.2. Nevertheless, there
is a script to do automatic conversion. See the file CHANGES on the ftp
server for a complete help on the new Auto/Hint syntax.

Summary of changes
=================
  Tactics
  -------
  - More proof techniques and more parametricity to use Auto (via
        the "Hint Extern" command)
  - "Intro x" now fails if "x" already exists in hypothesis (this may
    force to rewrite the tactic scripts which use this tolerance)

  Theories
  -------
  - A new theory : REALS, about axiomatised real numbers
  - the SORTING theory now works on polymorphic lists and trees
  - A new developpement LISTS/ListSet.v for finite sets implemented as lists.

  Directives
  ----------
  - Compiled ML file loading without Ocaml toplevel under Coq (bytecode only).

  Bug-fixes
  ---------
  - Bug-fixes about pretty-print and universes

  Tools
  -----
  - do_Makefile : new entries "gallinatex" and "gallinahtml" to pretty-print
  in LaTeX or HTML the vernacular files in the makefiles generated by
  do_Makefile

  - tools/dev/coqpath.el : one can use the Emacs tags to browse the Coq
   sources. To enable that functionnality, the user must :
     1) have a environment variable $COQTOP that points to the coq sources
     2) do : "make tags" in the $COQTOP directory
     3) Load coqpath.el under Emacs
        
     Then try "M-." and "C-u M-." !

Summary of incompatibilities
============================
  - New syntax for Hint and Auto (there is a conversion script, see below)
  - "Intro x" and "Intros x y z" less tolerant (generally few scripts
    are concerned, they must be changed at hand)

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

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

An updated version of the CtCoq interface should be soon available
http://www.inria.fr/croap/ctcoq/ctcoq-eng.html

Coq V6.2.3 is available as source code (Coq 6.2.3 requires the latest version 
of Ocaml and Camlp4 (2.01) to compile), binary distribution for linux/Intel, 
Solaris/Sparc, Digital Unix/Alpha and Windows NT/95.

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.