test-suite/bugs/closed/bug_9595.v


1
2
3
4
5
6
7
8
9
10
11

Set Primitive Projections.
Set Warnings "+non-primitive-record".

(* 0 fields *)
Fail Record foo := { a := 0 }.

(* anonymous field *)
Fail Record foo := { _ : nat }.

(* squashed *)
Fail Record foo : Prop := { a : nat }.