The Coq mailing list

[Hugo Herbelin <herbelin AT margaux.inria.fr>]

The Coq team is pleased to announce the availability of the new version 
of Coq: V6.3.1

This version is for bug-fixes and slight improvements in implicits
synthesis and speed.

Changes from V6.3
=================

Gallina:

- More type synthesis, especially in Cases, for term typable with
  simple types (roughly: ML typing algorithm without polymorphism)
- Mysterious "?" in Goal should now display the corresponding
  instantiation when it exists.
- Old .vo files are incompatible and should be recompiled.

Bug fixed:

- Tauto has been unable for a time to deal with hypotheses with 2
  imbricated implications. Now it should work.
- Intuition now removes true (therefore useless) hypotheses.
- Cofixpoint: a hole in the guardness condition when a cofixpoint
  refers to another one has been corrected.
  WARNING: the new criterion may refuse some olderly accepted
  Cofixpoint definitions which actually are valid but for a reason
  difficult to detect automatically (e.g. Udine's Pi-calculus
  contribution is currently rejected)
- Extraction: a bug was limiting the number of propositional singleton
  inductive types (such has "eq") for which elimination towards Set is
  valid.
- Several bugs of the Program tactic are fixed (but some automatically
  generated names have changed and may lead to incompatibilities).
- Time command bug fixed
- Bug with negative index in bindings fixed

Speed improvement:

- Redondant checks when applying a tactic have been turned off. For
  some tactics that don't make themselves the expected verifications, it
  may result in incorrect proofs detected only at Qed/Save time. In this
  last case, you can turn on the -tac-debug flag to coqtop.
- We recall that ocaml provides native code. To take benefit of it
  with Coq, you shoud call Coq with "coqtop -opt" or "coqtop -full"

Contributions:

- New contribution on Binary Decision Diagrams (BDDs) provided by
  Kumar Verma (Dyade)
- New contribution on a distributed reference counter (part of a
  garbage collector) provided by Jean Duprat (ENS-Lyon)

Look at the file CHANGES in the distribution for more details on
changes (e.g. sources of incompatibility for ocaml tactics).

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

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

or via http://coq.inria.fr

The following interfaces are available for Coq:
The graphic interface CtCoq (http://www.inria.fr/croap/ctcoq/ctcoq-eng.html)
The Proof General emacs mode (http://www.dcs.ed.ac.uk/home/proofgen)
Gang Chen graphic interface for Windows 95 (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