The Coq mailing list

[gallego AT cri.ensmp.fr (Emilio Jesús Gallego Arias)]

Abhishek Anand 
<abhishek.anand.iitg AT gmail.com>
 writes:

> I don't know about merlin, but you can use Ltac pattern matching and "type
> of" to conveniently find out types of sub-expressions.

I have also found quite useful ssreflect's

"set f := pattern"

tactic to find out types of tricky sub-expressions; the matching
mechanism usually works well for my full-of-holes patterns.

I don't know if this can be done with the standard Coq tactics.

Best regards,
Emilio