test-suite/bugs/closed/bug_11727.v


1
2
3
4
5
6
7
8

Tactic Notation "myunfold" reference(x) := unfold x.
Notation idnat := (@id nat).
Goal let n := 0 in idnat n = 0.
Proof.
  intro n.
  myunfold idnat.
  myunfold n.
Abort.