The Coq mailing list

[anoun AT labri.fr]

Thanks a lot,
Though the tactic is not generic (n should be < 6 in that case), I think that 
it
suits my needs
Houda
>
> > Pierre Letouzey posted the definition of such a tactic on this list
> > some time ago, check the list archives.
>
> The message Xavier is talking about is the following
>
> http://coq.inria.fr/mailing-lists/coqclub/200411/msg00047.html
>
>
> The fact that we can't write this kind of generic tactic directly using
> Ltac is a bit puzzling. One problem seems to be that Ltac
> doesn't accept currified terms in filters so
>
> 1 + 2 does not match ?f ?a
>
> it is not clear to me why Ltac imposes such a limitation. A
> workaround would be for Ltac to provide some destructor
> primitives so we would be able to code directly our own filtering.
> This could be sometimes handy.
>
> --
> Laurent Théry
>
>
>




----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.