Removing documentation related to the deprecated State machinery.

2 files changed, 0 insertions, 27 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index b010e6e182..3feabb2285 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -116,12 +116,6 @@ Section~\ref{LongNames}).
   conventional version control management sub-directories named {\tt
   CVS} and {\tt \_darcs} are excluded.
 
-\item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}, {\tt -outputstate} {\em file}]\ 
-
-  Load at the beginning/Dump at the end a \Coq{} state from the file {\em file}.
-
-  Incompatible with some not purely functional aspect of the code 
-
 \item[{\tt -nois}]\ 
 
   Cause \Coq~to begin with an empty state.
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 8aa6df0616..0a283776fd 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -895,27 +895,6 @@ extra commands and end on a state $\num' \leq \num$ if necessary.
   The destination state label is unknown.
 \end{ErrMsgs}
 
-\section{State files}
-
-\subsection[\tt Write State \str.]{\tt Write State \str.\comindex{Write State}}
-Writes the current state into a file \str{} for
-use in a further session. This file can be given as the {\tt
-  inputstate} argument of the commands {\tt coqtop} and {\tt coqc}.
-
-\begin{Variants}
-\item {\tt Write State \ident}\\
- Equivalent to {\tt Write State "}{\ident}{\tt .coq"}.
- The state is saved in the current directory (see Section~\ref{Pwd}).
-\end{Variants}
-
-\subsection[\tt Restore State \str.]{\tt Restore State \str.\comindex{Restore State}}
-  Restores the state contained in the file \str.
-
-\begin{Variants}
-\item {\tt Restore State \ident}\\
- Equivalent to {\tt Restore State "}{\ident}{\tt .coq"}.
-\end{Variants}
-
 \section{Quitting and debugging}
 
 \subsection[\tt Quit.]{\tt Quit.\comindex{Quit}}