The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

On Fri, Apr 29, 2011 at 11:45:11AM +0200, Arnaud Spiwack wrote:
> 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.

Thanks for your hard work, Arnaud!

I don't think it is related to your changes, but just for the record
    http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2371
is still broken, and IMO is a blocker for C-zar usage.


Thanks
Ian