From 78c2ebe640e86e7357982e6e07b8121111a51fcc Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 14 Dec 2015 15:16:35 +0100
Subject: Remove a mention of Set Virtual Machine in doc.

---
 doc/refman/RefMan-gal.tex | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 0e758bcab6..fcccd9cb4b 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}
-- 
cgit v1.2.3