test-suite/bugs/closed/bug_3520.v


1
2
3
4
5
6
7
8
9

Set Primitive Projections.

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

Set Nonrecursive Elimination Schemes.

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