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