From ab3a1aed8fcaed3b0988b686b7f4cf7124b07ab2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 11 Dec 2015 12:15:17 +0100
Subject: Remove Set Virtual Machine from doc, since the command itself has
 been removed.

---
 doc/refman/RefMan-com.tex | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'doc/refman/RefMan-com.tex')

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}
-- 
cgit v1.2.3