Better doc and a few fixes for Proof using.

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