2 files changed, 1 insertions, 35 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 5b1ad1981b..e79245b0e0 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -836,9 +836,7 @@ and we want to backtrack to a state labeled by:
 
 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).
+state 12 and finally go back to environment state 32.
 
 \begin{Variants}
 \item {\tt BackTo n}. \comindex{BackTo}\\
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 4fa845310c..884a1e6e72 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -34,9 +34,6 @@ isomorphism} \cite{How80,Bar91,Gir89,Hue89}, \Coq~ stores proofs as
 terms of {\sc Cic}. Those terms are called {\em proof
   terms}\index{Proof term}.
 
-It is possible to edit several proofs in parallel: see Section
-\ref{Resume}.
-
 \ErrMsg When one attempts to use a proof editing command out of the
 proof editing mode, \Coq~ raises the error message : \errindex{No focused
   proof}.
@@ -174,35 +171,6 @@ proof was edited.
 \end{Variants}
 
 %%%%
-\subsection[\tt Suspend.]{\tt Suspend.\comindex{Suspend}}
-
-This command applies in proof editing mode. It switches back to the
-\Coq\ toplevel, but without canceling the current proofs.
-
-%%%%
-\subsection[\tt Resume.]{\tt Resume.\comindex{Resume}\label{Resume}}
-
-This commands switches back to the editing of the last edited proof.
-
-\begin{ErrMsgs}
-\item \errindex{No proof-editing in progress}
-\end{ErrMsgs}
-
-\begin{Variants}
-
-\item {\tt Resume {\ident}.}
-
-  Restarts the editing of the proof named {\ident}. This can be used
-  to navigate between currently edited proofs.
-
-\end{Variants}
-
-\begin{ErrMsgs}
-\item \errindex{No such proof}
-\end{ErrMsgs}
-
-
-%%%%
 \subsection[\tt Existential {\num} := {\term}.]{\tt Existential  {\num} := {\term}.\comindex{Existential}
 \label{Existential}}