blob: 735fefd745e3b9adf45fb0ec02c19515f1c07bef (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
Require Import A.
Definition y := x.
Lemma yeq : y = y.
Proof. pose xeq. auto. Qed.
Section Foo.
Variable (HFalse : False).
Lemma yeq' : y = y.
Proof using HFalse. elimtype False. apply HFalse. Qed.
End Foo.
Module Type E. End E.
Module M.
Lemma x : True.
Proof. trivial. Qed.
End M.
Module Type T.
Lemma x : True.
Proof. trivial. Qed.
End T.
Module F(X:E).
Lemma x : True.
Proof. trivial. Qed.
End F.
|
