The Coq mailing list

[Pierre Corbineau <Pierre.Corbineau AT imag.fr>]

It is because the proof term is not as trivial as for a goal-only induction.

Le 07/12/2010 20:58, Ian Lynagh a écrit :
> On Mon, Dec 06, 2010 at 06:11:45PM +0100, AUGER Cedric wrote:
> > As often, it is very surprising that a 4 line proof in manual require
> > so much lines in Cezar (but also in normal mode, if you do not use
> > highly automated proofs).
> >
> > Is this mode "frozen" (with all these flaws) or is it not?
>
> Czar appears to be unmaintained, sadly.

I have tried to fix all bugs I (and others) have discovered over the 
years, but the one mentinned below as Arnaud Spiwack confessed,  was 
introduced when merging with the new proof engine and neither he nor I 
have found/taken the time to meet and fix it. Perhaps now could be the 
time ?

> There is at least one show-stopper for me:
>      http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2371
>
>
> Thanks
> Ian

--
Pierre Corbineau          | 
Pierre.Corbineau AT imag.fr
VERIMAG - Centre Équation | Tel: (+33 / 0) 4 56 52 04 42
2, avenue de Vignate      | Office nr B7
38610 GIÈRES - FRANCE     | http://www-verimag.imag.fr/~corbinea/
begin:vcard
fn:Pierre Corbineau
n:Corbineau;Pierre
org;quoted-printable:Universit=C3=A9 Joseph Fourier - Grenoble 1;Laboratoire VERIMAG - Polytech' Grenoble
adr;quoted-printable;quoted-printable:2, avenue de Vignate;;VERIMAG - Centre =C3=89QUATION ;GI=C3=88RES ;;38610;France
email;internet:Pierre.Corbineau AT imag.fr
title;quoted-printable:Ma=C3=AEtre de Conf=C3=A9rences
tel;work:+33 (0) 4 56 52 04 42
tel;fax:+33 (0) 4 56 52 03 44
x-mozilla-html:FALSE
url:http://www-verimag.imag.fr/~corbinea
version:2.1
end:vcard

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature