From de0085539583f59dc7c4bf4e272e18711d565466 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Thu, 13 Jul 2006 14:28:31 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta.2

---
 doc/refman/RefMan-pro.tex | 19 ++++++-------------
 1 file changed, 6 insertions(+), 13 deletions(-)

(limited to 'doc/refman/RefMan-pro.tex')

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 739ca6b5..8c1a7824 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}
@@ -381,7 +374,7 @@ All the hypotheses remains usable in the proof development.
 This command goes back to the default mode which is to print all
 available hypotheses.
 
-% $Id: RefMan-pro.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $
+% $Id: RefMan-pro.tex 9030 2006-07-07 15:37:23Z herbelin $
 
 %%% Local Variables: 
 %%% mode: latex
-- 
cgit v1.2.3

