diff options
Diffstat (limited to 'doc/refman/RefMan-gal.tex')
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 5 |
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} |