Remove a mention of Set Virtual Machine in doc.

1 files changed, 2 insertions, 3 deletions

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 0e758bcab..fcccd9cb4 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -496,9 +496,8 @@ arguments is used for making explicit the value of implicit arguments
 The expression ``{\term}~{\tt :}~{\type}'' is a type cast
 expression. It enforces the type of {\term} to be {\type}.
 
-``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine (as if option
-{\tt Virtual Machine} were on, see \ref{SetVirtualMachine}) for checking that
-{\term} has type {\type}.
+``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine for checking
+that {\term} has type {\type}.
 
 \subsection{Inferable subterms
 \label{hole}