The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On 14 Jan 2004 16:03:40 +0100
maggesi AT math.unice.fr
 (Marco.MAGGESI) wrote:

> 
> Hi,
> 
> This version of "Congr" is a "quick hack" but works pretty well in
> practice.  It has several limitations that I would like to remove but
> I do not know how do that in a simple way using the tactic language.
> In particular, it works only for equations of the form
> 
>   f x_1 ... x_n = f y_1 ... y_n
> 
> where n <= 6.  The problem is that I cannot get around the fact that
> match doesn't work with curried functions.
> 
> Any idea?


I gave the same tactic and signal the same problem some month ago on this
list. As far as I know Ltac may deal with curried function one day, but not
yet. If you really need to deal with any number of args (you probably
don't), your only option is to write your tactic in ocaml.

Cheers,
Pierre Courtieu