aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3520.v
blob: c981207e6bfb91f6defafd5052941fc3cf79dd1b (plain)
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 }.