Proof using ...

New vernacular "Proof using idlist" to declare the variables
to be discharged at the end of the current proof. The system
checks that the set of declared variables is a superset of
the set of actually used variables.

It can be combined in a single line with "Proof with":
Proof with .. using ..
Proof using .. with ..

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7

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 0000000000..93a9ef1161
--- /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).
+