Coq distribution

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]


We are glad to announce the release of version 5.10.15 of the Coq
Proof Assistant for the Calculus of Inductive Constructions. This release
includes various changes in the code and libraries, which are
described more precisely below. The documentation has also been

Coq V5.10.15 comes in two flavors: the regular Coq, and a new, fully
up-to-date and compatible distribution of Ct-Coq (i.e. Coq with a
sophisticated graphical user-interface).

The Coq distribution is available at Rocquencourt and in Lyon:

or through:

As usual, get the README files first, for instructions.

Because the organization of some files and directories has changed, we
will not provide any patches for update.

Ct-coq is available in Sophia-Antipolis:


Below, you will find a summary of the main changes with respect to the
previous version. It is followed by a description of the new Ct-Coq by
Janet Bertot. 

This concerns the UNIX version of V5.10.15.
For the Microsoft-Windows as well as the Macintosh version
see below.

As usual, you might send problems, bug reports, remarks about the
installation to
and more general questions about the coq system to the mailing list
questions specific to the Ct-Coq interface should be addressed to


 for the Coq team,

Gerard Huet 

(*  Main changes between V5.10.14 (july 95) and V5.10.15 (feb 96)   *)

* Changes in code:
- (x:A)(y:A)B is now printed as (x,y:A), same for abstraction.
- Many internal bugs have been fixed.
- New commands Set/Unset Undo to control the number of possible undo
               Set/Unset Hyps_limit to control the number of printed hypotheses
* Changes in tactics:
- New tactics Rewrite .. in
- More inversion tactics (see the reference manual)
  1) The tactics (Derive) Inversion and (Derive) Inversion_clear have been
     extended to (co)inductive types of sort Set and Type.
  2) New tactics are available for deriving inversion lemmas on different 
     sorts and performing simple dependent inversion.
- The tactic Rewrite uses now the lemmas eq_ind_r and no more the symmetry.

* The reference manual has been updated.

* Changes in librairies :
- Some Hint/Immediate have been added in the basic theories.
- More results on classical logic (previously in INIT/Classical) 
  are now in the directory theories/LOGIC
- theories/RELATIONS contains basic definitions and properties on relations 
  while theories/RELATIONS/WELLFOUNDED establishes results on well-foundness.
- Changes in the development theories/ALGEBRA
- A new directory theories/SORTING has been added.

* New contributions :


Subject: CtCoq (running with Coq v5.10.15 -- archive of 15 February 1996)

CtCoq provides a working environment for the Coq theorem prover,
via a graphical user interface.  The X interface and Coq run as 
separate processes and the interface has multiple fonts and colors
for displaying commands, it provides support for constructing commands
and formulae, has an experimental textual presentation of proofs, and, 
using a technique called "Proof by Pointing", allows the user to direct
the proof by clicking with the mouse on various parts of the subgoals.
To find out more, visit our www page listed below.

The CtCoq user interface version "beta2", which runs with Coq version 
5.10.15, is now available for both sun4OS4 and DecAlpha workstations.   


New features in this version of CtCoq include:

    o Comments are handled partially, i.e., when associated to a toplevel 
      command.  (NB: This works only if you have "perl" on your system.)

    o The "Discard" interface has been extended so that the Discard button
      may be used for undoing commands *other* than proof steps.  Thus, one
      can discard theorems, axioms, or definitions.  Still certain commands
      (such as Require or Hint) cannot be undone.

    o Parsing of subexpressions in the Command window is no longer limited
      to commands, tactics, or formulae, allowing for finer text editing.
    o Proof by Pointing behavior has been improved.  The generated script is
      more natural for Coq users.

    o Menus used in guided editing are now complete (updated for V5.10.15 
      syntax).  Transformations between different variants of a command 
      or tactic are provided.  The presentation of the hierarchical menus
      has changed, hopefully making guided editing more agreeable.

    o The auto-saving capability has been improved, making it less disruptive.


The www page is:


The direct ftp route is:

        The machine:    babar.inria.fr (
        The directory:  pub/centaur/ctcoq-beta2

        Follow the README instructions to obtain all that you need.
        NB: if you obtain the system directly by ftp you should send
            mail to ctcoq-request@sophia.inria.fr indicating for which 
            architecture(s) you wish to run the CtCoq system.

For all and any questions/problems please send mail to:


          HOT        ! Last minute !        HOT


The latest version 5.10.15 of Coq is now also available for PC's running
Microsoft Windows 95 or Windows NT, as well as for the Apple Macintosh
(with 68k or PPC architecture).

These releases are as close as possible to the UNIX versions. There
can be found in the usual ftp directory in Rocquencourt:




Both distributions do not contain the user's contributions. You might
however use and add the corresponding files from the unix distrib.

As usual, please send any comments, bug reports, questions, to

The Windows version is due to Henri Laulhere; the Macintosh one to
Cesar Munoz.


Coming soon: arithmetic decision tactics.