The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Given the name of a function with implicit args, say "foo", the name 
"@foo" names the same function with all args made explict.  However, the 
"@" does not seem to be an operator that one can apply to a name 
tactically.  For example - the following doesn't work:

Tactic Notation "Explicitly" uconstr(L) := pose proof @L.

as it appears to ignore the "@", with the result that pose proof fails 
due to uninferrable implicits.

Is there any way to take a name of a function and tactically change it 
to its explicit version?

-- Jonathan