bug_4638.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/bugs/closed/bug_4638.v

blob: 951fe5302b839466278edeef8c7cfb42ed3b0ee8 (plain)

Set Nested Proofs Allowed.

Class Foo.

Goal True.

Instance foo: Foo.
Qed.

trivial.

Qed.