aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3899.v
blob: 7754934c0b90644be7f2b434d2d9556e5e4b6a5c (plain)
1
2
3
4
5
6
7
8
9
10
11
Set Primitive Projections.
Record unit : Set := tt {}.
Fail Check fun x : unit => eq_refl : tt = x.
Fail Check fun x : unit => eq_refl : x = tt.
Fail Check fun x y : unit => (eq_refl : x = tt) : x = y.
Fail Check fun x y : unit => eq_refl : x = y.

Record ok : Set := tt' { a : unit }.

Record nonprim : Prop := { undef : unit }.
Record prim : Prop := { def : True }.