2 files changed, 0 insertions, 26 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 9862abb53..8bb1cc331 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -87,7 +87,6 @@ code. The list of highlight tags can be retrieved with the {\tt -list-tags}
 command-line option of {\tt coqtop}.
 
 \subsection{By command line options\index{Options of the command line}
-\label{vmoption}
 \label{coqoptions}}
 
 The following command-line options are recognized by the commands {\tt
@@ -224,11 +223,6 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
 \item[{\tt -no-hash-consing}] \mbox{}
 
-\item[{\tt -vm}]\ 
-
-  This activates the use of the bytecode-based conversion algorithm
-  for the current session (see Section~\ref{SetVirtualMachine}).
-
 \item[{\tt -image} {\em file}]\ 
 
   This option sets the binary image to be used by {\tt coqc} to be {\em file}
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 4b2b8660c..0a243308d 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -1075,26 +1075,6 @@ perform a {\tt Ltac \ident\ := {\rm\sl convtactic}}.
 
 \SeeAlso sections \ref{Conversion-tactics}
 
-\subsection{\tt Set Virtual Machine
-\label{SetVirtualMachine}
-\optindex{Virtual Machine}}
-
-This activates the bytecode-based conversion algorithm.
-
-\subsection{\tt Unset Virtual Machine
-\optindex{Virtual Machine}}
-
-This deactivates the bytecode-based conversion algorithm.
-
-\subsection{\tt Test Virtual Machine
-\optindex{Virtual Machine}}
-
-This tells if the bytecode-based conversion algorithm is
-activated. The default behavior is to have the bytecode-based
-conversion algorithm deactivated.
-
-\SeeAlso sections~\ref{vmcompute} and~\ref{vmoption}.
-
 \section{Controlling the locality of commands}
 
 \subsection{{\tt Local}, {\tt Global}