aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_3890.v
blob: e1823ac54c12d289504b1acb842360fcef53b2fc (plain)
1
2
3
4
5
6
7
8
9
10
11
12
Set Nested Proofs Allowed.

Class Foo.
Class Bar := b : Type.

Instance foo : Foo.

Instance bar : Bar.
exact Type.
Defined.

Defined.