diff options
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). + |