The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

> 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