Remove Set Virtual Machine from doc, since the command itself has been removed.

1 files changed, 0 insertions, 6 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 9862abb533..8bb1cc331b 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}