test-suite/bugs/opened/3277.v


1
2
3
4
5
6
7

Tactic Notation "evarr" open_constr(x) := let y := constr:(x) in exact y.

Goal True.
  evarr _.
Admitted.
Goal True.
  Fail exact ltac:(evarr _). (* Error: Cannot infer this placeholder. *)