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

2 files changed, 28 insertions, 0 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index c781c82747..e5dc669dd5 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -133,6 +133,24 @@ one gulp, as a proof term (see Section~\ref{exact}).
 
 \SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}.
 
+\subsection[\tt Proof using {\ident$_1$ \dots {\ident$_n$}}.]
+{\tt Proof using {\ident$_1$ \dots {\ident$_n$}}.
+\comindex{Proof using} \label{ProofUsing}}
+
+This command applies in proof editing mode. 
+It declares the set of section variables (see~\ref{Variable}) 
+used by the proof. At {\tt Qed} time, the system will assert that 
+the set of section variables actually used in the proof is a subset of
+the declared one.
+
+The set of declared variables is closed under type dependency.
+For example if {\tt T} is variable and {\tt a} is a variable of
+type {\tt T}, the commands {\tt Proof using a} and
+{\tt Proof using T a} are actually equivalent.
+
+\variant {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}.} 
+in Section~\ref{ProofWith}.
+
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
 
 This command cancels the current proof development, switching back to
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d0c193de1b..198f8f3043 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4239,6 +4239,16 @@ e.g. \texttt{Require Import A.}).
 
 \SeeAlso {\tt Proof.} in Section~\ref{BeginProof}.
 
+\begin{Variants}
+\item {\tt Proof with {\tac} using {\ident$_1$ \dots {\ident$_n$}}}
+  Combines in a single line {\tt Proof with} and {\tt Proof using}, 
+  see~\ref{ProofUsing}
+\item {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}}
+  Combines in a single line {\tt Proof with} and {\tt Proof using}, 
+  see~\ref{ProofUsing}
+
+\end{Variants}
+
 \subsubsection[\tt Declare Implicit Tactic {\tac}.]{\tt Declare Implicit Tactic {\tac}.\comindex{Declare Implicit Tactic}}
 
 This command declares a tactic to be used to solve implicit arguments