Documentation machine virtuelle

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9044 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 730100eedd..64f99835b6 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}