test-suite/bugs/closed/3520.v


1
2
3
4
5
6
7
8
9
10
11
12

Set Primitive Projections.

Record foo (A : Type) := 
  { bar : Type ; baz := Set; bad : baz = bar }.

Set Record Elimination Schemes.

Record notprim : Prop :=
  { irrel : True; relevant : nat }.