Skip to Content.
Sympa Menu

coq-club - Release of Coq V6.2.1

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Release of Coq V6.2.1


chronological Thread 
  • From: Christine Paulin <Christine.Paulin AT lri.fr>
  • To: coq-club AT pauillac.inria.fr
  • Subject: Release of Coq V6.2.1
  • Date: Thu, 23 Jul 1998 16:47:15 +0200 (MEST)


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

6.2.1 is mainly a bug-fix release. Several important bugs have been 
corrected, and minor speed improvements (in typing or extraction) were
realized. The changes are : 

- Bug-fixes in the Omega and Ring tactics
- more precise syntax of integer expressions. For example  
  `(Zinv 1)` is printed as is and no more `-1` : this avoid confusion.
  (Zinv x) is still printed `-x`.  
- Extraction now generates less universes and is more efficient
- the tactic Auto is somewhat faster (Auto in V6.2 was much slower
  than in V6.2.beta) . 
  "Print Hint" has a new meaning : it displays the hints that apply to
  the current goal. "Print Hint *" has replaced the old command "Print
  Hint" and prints all hints. 
- Programs has been much debugged, but it is still in beta-test. It is
  now included in the documentation 
- "if then else" and "let in" expessions are now printed as they are
  parsed - several error messages are now more explicit 
- Bug-fixes in unification and in Program 
- Printing of tactic scripts is nicer 
- "make install" now allowed with do_Makefile 
- new commands "Set Printing Depth/Print Printing Depth" 
- Improvements of the chapter "Writing you own tactics" of the doc


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 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/lego/html/emacs-2.0.html

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.1 is available as source code, binary distribution for linux/Intel, 
Solaris/Sparc, Digital Unix/Alpha and Windows NT/95 (soon 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






Archive powered by MhonArc 2.6.16.

Top of Page