test-suite/output-coqchk/bug_5030.v


1
2
3
4
5
6
7
8
9
10

Module Type testt.
Parameter proof : True.
End testt.

Module Export test : testt.
Definition proof := I.
End test.

Lemma true : True.
Proof. apply proof. Qed.