From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/success/proof_using.v | 53 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 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 bf302df4..dbbd57ae 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -65,3 +65,56 @@ End S1. Check (deep 3 4 : 3 = 4). Check (deep2 3 4 : 3 = 4). + +Section P1. + +Variable x : nat. +Variable y : nat. +Variable z : nat. + + +Collection TOTO := x y. + +Collection TITI := TOTO - x. + +Lemma t1 : True. Proof using TOTO. trivial. Qed. +Lemma t2 : True. Proof using TITI. trivial. Qed. + + Section P2. + Collection TOTO := x. + Lemma t3 : True. Proof using TOTO. trivial. Qed. + End P2. + +Lemma t4 : True. Proof using TOTO. trivial. Qed. + +End P1. + +Lemma t5 : True. Fail Proof using TOTO. trivial. Qed. + +Check (t1 1 2 : True). +Check (t2 1 : True). +Check (t3 1 : True). +Check (t4 1 2 : True). + + +Section T1. + +Variable x : nat. +Hypothesis px : 1 = x. +Let w := x + 1. + +Set Suggest Proof Using. + +Set Default Proof Using "Type". + +Lemma bla : 2 = w. +Proof. +admit. +Qed. + +End T1. + +Check (bla 7 : 2 = 8). + + + -- cgit v1.2.3