aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/opened/3277.v
blob: 19ed787d1e1ab47d03e08a8b64300fd1c8e6f61e (plain)
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 $(evarr _)$. (* Error: Cannot infer this placeholder. *)