diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /test-suite/success/proof_using.v | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'test-suite/success/proof_using.v')
-rw-r--r-- | test-suite/success/proof_using.v | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v new file mode 100644 index 00000000..93a9ef11 --- /dev/null +++ b/test-suite/success/proof_using.v @@ -0,0 +1,61 @@ +Section Foo. + +Variable a : nat. + +Lemma l1 : True. +Fail Proof using non_existing. +Proof using a. +exact I. +Qed. + +Lemma l2 : True. +Proof using a. +Admitted. + +Lemma l3 : True. +Proof using a. +admit. +Qed. + +End Foo. + +Check (l1 3). +Check (l2 3). +Check (l3 3). + +Section Bar. + +Variable T : Type. +Variable a b : T. +Variable H : a = b. + +Lemma l4 : a = b. +Proof using H. +exact H. +Qed. + +End Bar. + +Check (l4 _ 1 1 _ : 1 = 1). + +Section S1. + +Variable v1 : nat. + +Section S2. + +Variable v2 : nat. + +Lemma deep : v1 = v2. +Proof using v1 v2. +admit. +Qed. + +End S2. + +Check (deep 3 : v1 = 3). + +End S1. + +Check (deep 3 4 : 3 = 4). + |