Documentation Declare Implicit Tactic, Print Canonical Projections, ... + légère restructuration autour de Proof with et Hint Rewrite + maj crédits

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

1 files changed, 5 insertions, 12 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 7565612d1..ddfce775d 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -163,28 +163,21 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels:
   current section.
 \end{Variants}
 
-\subsection{\tt Proof {\term}.}\comindex{Proof}
+\subsection{\tt Proof {\term}.}
+\comindex{Proof}
+\label{BeginProof}
 This command applies in proof editing mode. It is equivalent to {\tt
   exact {\term}; Save.} That is, you have to give the full proof in
 one gulp, as a proof term (see section \ref{exact}).
 
-\begin{Variants}
-
-\item{\tt Proof.}
+\variant {\tt Proof.}
   
   Is a noop which is useful to delimit the sequence of tactic commands
   which start a proof, after a {\tt Theorem} command.  It is a good
   practice to use {\tt Proof.} as an opening parenthesis, closed in
   the script with a closing {\tt Qed.}
 
-\item{\tt Proof with {\tac}.}
-  
-  This command may be used to start a proof. It defines a default
-  tactic to be used each time a tactic command is ended by
-  ``\verb#...#''. In this case the tactic command typed by the user is
-  equivalent to \emph{command};{\tac}.
-
-\end{Variants}
+\SeeAlso {\tt Proof with {\tac}.} in section~\ref{ProofWith}.
 
 \subsection{\tt Abort.}
 \comindex{Abort}