test-suite/bugs/closed/bug_10669.v


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

Context (A0:Type) (B0:A0).
Definition foo0 := B0.

Set Universe Polymorphism.
Context (A1:Type) (B1:A1).
Definition foo1 := B1.

Section S.
  Context (A2:Type) (B2:A2).
  Definition foo2 := B2.
End S.