coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A message to C-zar users

From: Arnaud Spiwack <arnaud AT spiwack.net>
To: coq-club AT inria.fr
Subject: [Coq-Club] A message to C-zar users
Date: Fri, 29 Apr 2011 11:45:11 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; b=ZSEs9/tepDKUObBzDqw7ADCkRMgiJpAsZkaVNS80aEs8Cay4cBrhu/Aklt7VclaGhi bHiGZyM8aOWm6zX2UIE1e7dWgJUTIS3bWgLO4jAUxtgxDTQIQhsOOpDKzP2ld0m2DV8C eLOQgfVHpCJfcdGQiNENKT+q9Uf4rj8vwKJBY=

The declarative proof mode (C-zar) of Coq, which had been mostly not working in Coq's trunk for a few month, should now be fully repaired. If you are a trunk+C-zar user, it is now pretty safe to update your Coq. However, some of my fixes are a bit clumsy, I wouldn't be surprised if some undesirable behaviour has escaped our standard tests. Please report such issues, so that the approaching release packs a pristine version of C-zar.

Best,

Arnaud Spiwack

[Coq-Club] A message to C-zar users, Arnaud Spiwack
- Re: [Coq-Club] A message to C-zar users, Ian Lynagh