test-suite/bugs/closed/bug_9494.v


1
2
3
4
5
6
7
8
9
10

Lemma foo (a : nat) : True.
Proof.
destruct a eqn:n; exact I.
Qed.

Set Mangle Names.
Lemma foo2 (a : nat) : True.
Proof.
let N := fresh in destruct a eqn:N; exact I.
Qed.