coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "suppose it is ... with" in C-zar

From: Pierre Corbineau <Pierre.Corbineau AT imag.fr>
To: Lauri Alanko <lealanko AT cs.helsinki.fi>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] "suppose it is ... with" in C-zar
Date: Thu, 22 Oct 2009 14:18:06 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Mailscanner-null-check: 1256818686.97723@qrvbtof83CAvSFiAzU83/w
Organization: Verimag

Could you be more specific

Lauri Alanko a �crit :

Hello.

I'm using Coq 8.2pl1. Occasionally when trying to do induction in
C-zar, a "suppose it is" -instruction yields the error:

Error: Wrong number of extra arguments: 1expected.

Could you be more specific than "occasionnaly", i.E. give a file producing the error message.

Regards,

Pierre

--
Pierre Corbineau          |
Pierre.Corbineau AT imag.fr
VERIMAG - Centre �quation | Tel: (+33 / 0) 4 56 52 04 42
2, avenue de Vignate      | Office nr B2G2
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

[Coq-Club] "suppose it is ... with" in C-zar, Lauri Alanko
- Re: [Coq-Club] "suppose it is ... with" in C-zar, Pierre Corbineau