From de0085539583f59dc7c4bf4e272e18711d565466 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Thu, 13 Jul 2006 14:28:31 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta.2

---
 doc/refman/RefMan-com.tex | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

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

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index f8a7546f..8c54e0ed 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -86,6 +86,7 @@ you move the \Coq\ binaries and library after installation.
 
 \section{Options}
 \index{Options of the command line}
+\label{vmoption}
 
 The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}, unless stated otherwise:
@@ -239,6 +240,11 @@ The following command-line options are recognized by the commands {\tt
   resulting in a smaller memory requirement and faster compilation;
   warning: this invalidates some features such as the extraction tool.
 
+\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 to be {\em file}
@@ -272,7 +278,7 @@ The following command-line options are recognized by the commands {\tt
 %   (see section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}).
 % \end{description}
 
-% $Id: RefMan-com.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ 
+% $Id: RefMan-com.tex 9044 2006-07-12 13:22:17Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
-- 
cgit v1.2.3