The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Does this do what you want?

Tactic Notation "with_open" open_constr(v) tactic3(tac) := tac v.

Tactic Notation "foo'" uconstr(v) tactic3(foo2) :=
  first [ let v' := constr:v in tryif has_evar v' then fail else pose proof v
        | with_open v foo2 ].

Ltac foo2 v :=
    idtac;
    match v with
      | ?f _ => foo' f foo2
      | _ => fail 1
    end.

Tactic Notation "head_pose_proof" uconstr(v) := foo' v foo2.

Goal True -> True.
  intro H.
  head_pose_proof eq_refl.

Or, if you want something simpler:

Ltac head x :=
  match x with
    | ?f _ => head f
    | _ => constr:x
  end.

Tactic Notation "head_pose_proof" open_constr(v) := let v' := head v in pose proof v'.

which may or may not have the behavior you want on things with explicit arguments already passed.

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