"suppose it is ... with" in C-zar

[Lauri Alanko-3]

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.

From quick perusing of the sources, it seems that these "extra
arguments" are something that are supposed to be given in a
"with"-clause after the case pattern. However, its usage doesn't seem
to be documented anywhere, and in fact trying to use "with" gives a
syntax error (which is mysterious, since I can see that it has been
included in the grammar in g_decl_mode.ml4).

Could someone shed light on the nature of the error message and the
intended use of the with-clause? Thanks.


Lauri

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Pierre Corbineau-2]

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@...
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/

[Pierre_Corbineau.vcf]

---

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@...
title;quoted-printable:Ma=C3=AEtre de Conf=C3=A9rences
tel;work:[phone]
tel;fax:[phone]
x-mozilla-html:FALSE
url:http://www-verimag.imag.fr/~corbinea
version:2.1
end:vcard

---