From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- test-suite/success/proof_using.v | 76 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 76 insertions(+) (limited to 'test-suite/success/proof_using.v') diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index 61e73f85..c83f45e2 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -117,5 +117,81 @@ End T1. Check (bla 7 : 2 = 8). +Section A. +Variable a : nat. +Variable b : nat. +Variable c : nat. +Variable H1 : a = 3. +Variable H2 : a = 3 -> b = 7. +Variable H3 : c = 3. + +Lemma foo : a = a. +Proof using Type*. +pose H1 as e1. +pose H2 as e2. +reflexivity. +Qed. + +Lemma bar : a = 3 -> b = 7. +Proof using b*. +exact H2. +Qed. + +Lemma baz : c=3. +Proof using c*. +exact H3. +Qed. + +Lemma baz2 : c=3. +Proof using c* a. +exact H3. +Qed. + +End A. + +Check (foo 3 7 (refl_equal 3) + (fun _ => refl_equal 7)). +Check (bar 3 7 (refl_equal 3) + (fun _ => refl_equal 7)). +Check (baz2 99 3 (refl_equal 3)). +Check (baz 3 (refl_equal 3)). + +Section Let. + +Variables a b : nat. +Let pa : a = a. Proof. reflexivity. Qed. +Unset Default Proof Using. +Set Suggest Proof Using. +Lemma test_let : a = a. +Proof using a. +exact pa. +Qed. + +Let ppa : pa = pa. Proof. reflexivity. Qed. + +Lemma test_let2 : pa = pa. +Proof using Type. +exact ppa. +Qed. + +End Let. + +Check (test_let 3). + +Section Clear. + +Variable a: nat. +Hypotheses H : a = 4. + +Set Proof Using Clear Unused. + +Lemma test_clear : a = a. +Proof using a. +Fail rewrite H. +trivial. +Qed. + +End Clear. + -- cgit v1.2.3