test-suite/bugs/closed/bug_4574.v


1
2
3
4
5
6
7
8

Require Import Setoid.

Definition block A (a : A) := a.

Goal forall A (a : A), block Type nat.
Proof.
Fail reflexivity.
Abort.