The Coq mailing list

[CJ Bell <siegebell+coq AT gmail.com>]

This seems to work in 8.4pl4 at least:

Tactic Notation "Explicitly" constr(L) := pose proof L.  (* fallback tactic if L is not a global reference *)

Tactic Notation "Explicitly" reference(L) := pose proof L. (* poses global identifiers *)

I'm not very familiar with the "reference" argument type, so I don't know whether it will always work for you :/

-cj

On Thu, Nov 12, 2015 at 11:35 AM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

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