test-suite/bugs/closed/bug_12928.v


1
2
3
4
5
6
7

Lemma test: forall (x:bool) (x: nat), nat.
Proof. intros y x; abstract (exact x). Qed.

Set Mangle Names.
Lemma test': forall x : nat, nat.
Proof. intros x. abstract exact x. Qed.