diff options
Diffstat (limited to 'test-suite/success/proof_using.v')
| -rw-r--r-- | test-suite/success/proof_using.v | 28 |
1 files changed, 25 insertions, 3 deletions
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index d2691e7636..dbbd57ae0d 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -73,15 +73,15 @@ Variable y : nat. Variable z : nat. -Package TOTO := x y. +Collection TOTO := x y. -Package TITI := TOTO - x. +Collection TITI := TOTO - x. Lemma t1 : True. Proof using TOTO. trivial. Qed. Lemma t2 : True. Proof using TITI. trivial. Qed. Section P2. - Package TOTO := x. + Collection TOTO := x. Lemma t3 : True. Proof using TOTO. trivial. Qed. End P2. @@ -96,3 +96,25 @@ 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). + + + |