aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1977.v
blob: 28715040cef8f05ca403f904151f14a198ed12b5 (plain)
1
2
3
4
Inductive T {A} : Prop := c : A -> T.
Goal (@T nat).
apply c. exact 0.
Qed.