The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Houda Anoun wrote:

> Ltac elimTac0 lem:=   match goal with H : ?n>0 |- _ =>elim (lem n H) end.
>
> How can we solve this problem by defining a generic tactic that can 
> infer the arguments of the lemma which appear in the premiss H??


You can try
Ltac elimTac lem:= match goal with H : ?n>0 |- _ => elim lem with (1:=H) 
end.
It will set the first non-dependent argument of lem to H and in your 
second example it will find the correct instantation for n and m.

Bruno.