path: root/test-suite/bugs/closed/4378.v

Tactic Notation "epose" open_constr(a) :=
  let a' := fresh in
  pose a as a'.
Tactic Notation "epose2" open_constr(a) tactic3(tac) :=
  let a' := fresh in
  pose a as a'.
Goal True.
  epose _. Undo.
  epose2 _ idtac.