Changes in Backtrack documentation. More accurate.

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

1 files changed, 43 insertions, 30 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index bc098ef91..4df212f9e 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -724,39 +724,47 @@ file are considered as a single command.
 \subsection[\tt Backtrack $\num_1$ $\num_2$ $\num_3$.]{\tt Backtrack $\num_1$ $\num_2$ $\num_3$.\comindex{Backtrack}}
 
 This command is dedicated for the use in graphical interfaces.  It
-allows to backtrack to a particular \emph{global} state. Typically a
-state corresponding to a previous line in a script, which includes
-declaration environment but also proof environment (see
-chapter~\ref{Proof-handling}). The three numbers $\num_1$, $\num_2$
-and $\num_3$ represent the following:
+allows to backtrack to a particular \emph{global} state, i.e.
+typically a state corresponding to a previous line in a script. A
+global state includes declaration environment but also proof
+environment (see chapter~\ref{Proof-handling}). The three numbers
+$\num_1$, $\num_2$ and $\num_3$ represent the following:
 \begin{itemize}
-\item How many \texttt{Abort} (currently opened nested proofs that must
-  be forgotten) must be done ($\num_3$). 
-\item Which proof state must be unburied ($\num_2$) (once aborts have
-  been done).
-\item Which declaration environment state must be unburied ($\num_1$).
+\item $\num_3$: Number of \texttt{Abort} to perform, i.e. the number
+  of currently opened nested proofs that must be cancelled (see
+  chapter~\ref{Proof-handling}).
+\item $\num_2$: \emph{Proof state number} to unbury once aborts have
+  been done. Coq will compute the number of \texttt{Undo} to perform
+  (see chapter~\ref{Proof-handling}).
+\item $\num_1$: Environment state number to unbury, Coq will compute
+  the number of \texttt{Back} to perform.
 \end{itemize}
 
-Proof state and environment state are represented by numbers. Notice
-that these numbers are displayed in \Coq\ prompt when in
-\texttt{-emacs} mode. More precisely the prompt in \texttt{-emacs}
-mode is the following:
 
-\verb!<prompt>! \emph{curpr} \verb!<! $\num_1$
-\verb!|! \emph{currently opened proofs}
+\subsubsection{How to get state numbers?}
+\label{sec:statenums}
+
+
+Notice that when in \texttt{-emacs} mode, \Coq\ displays the current
+proof and environment state numbers in the prompt. More precisely the
+prompt in \texttt{-emacs} mode is the following:
+
+\verb!<prompt>! \emph{$id_i$} \verb!<! $\num_1$
+\verb!|! $id_1$\verb!|!$id_2$\verb!|!\dots\verb!|!$id_n$
 \verb!|! $\num_2$ \verb!< </prompt>!
 
 Where:
 
 \begin{itemize}
-\item \emph{curpr} is the name of the current proof (if there is
+\item \emph{$id_i$} is the name of the current proof (if there is
   one, otherwise \texttt{Coq} is displayed, see
 chapter~\ref{Proof-handling}).
 \item $\num_1$ is the environment state number after the last
   command.
-\item $\num_2$ is the current proof state number.
-\item \emph{currently opened proofs} is a \verb!|!-separated list of
-  currently opened  proof names.
+\item $\num_2$ is the proof state number after the last
+  command.
+\item $id_1$ $id_2$ \dots $id_n$ are the currently opened proof names
+  (order not significant).
 \end{itemize}
 
 It is then possible to compute the \texttt{Backtrack} command to
@@ -764,22 +772,27 @@ unbury the state corresponding to a particular prompt. For example,
 suppose the current prompt is:
 
 \verb!<! goal4 \verb!<! 35
-\verb!|! goal1 goal2 goal4 goal3 
-\verb!|! 8 \verb!< </prompt>!
+\verb!|!goal1\verb!|!goal4\verb!|!goal3\verb!|!goal2\verb!|! 
+\verb!|!8 \verb!< </prompt>!
 
 and we want to backtrack to a state labelled by:
 
 \verb!<! goal2 \verb!<! 32
-\verb!|! goal1 goal2
-\verb!|! 12 \verb!< </prompt>!
+\verb!|!goal1\verb!|!goal2
+\verb!|!12 \verb!< </prompt>!
 
-We have to perform \verb!Backtrack 32 12 2!, i.e. go to environment
-state 32, do 2 Aborts (to cancel goal4 and goal3) and undo proof until
-state 12.
+We have to perform \verb!Backtrack 32 12 2! , i.e. perform 2
+\texttt{Abort}s (to cancel goal4 and goal3), then rewind proof until
+state 12 and finally go back to environment state 32. Notice that this
+supposes that proofs are nested in a regular way (no \texttt{Resume} or
+\texttt{Suspend} commands).
 
-\subsection[\tt BackTo.]{\tt BackTo n.\comindex{BackTo}}
-Is a more basic form of \texttt{Backtrack} where only the first
-argument (global environment number) is given.
+\begin{Variants}
+\item {\tt BackTo n}. \comindex{BackTo}\\
+  Is a more basic form of \texttt{Backtrack} where only the first
+  argument (global environment number) is given, no \texttt{abort} and
+  no \texttt{Undo} is performed.
+\end{Variants}
 
 \subsection[\tt Restore State \str.]{\tt Restore State \str.\comindex{Restore State}}
   Restores the state contained in the file \str.