The Coq mailing list

[Lauri Alanko <lealanko AT cs.helsinki.fi>]

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