The Coq mailing list

[frederic.blanqui AT loria.fr]

hello. it is possible to apply some built-in tactics in some hypothesis using 
the "in" keyword. but it does not seem possible to do the same for 
user-defined (with ltac) tactics. is there a way to do that i do not know? 
otherwise, would it be difficult to add this in coq? thanks.