diff options
| author | Pierre-Marie Pédrot | 2015-12-11 13:02:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-11 13:06:53 +0100 |
| commit | 50d241267e2eb41cb06eb2f48a5ce440f0458b71 (patch) | |
| tree | f5d7c15cd62cf41177f2f902559ff21fc2988c54 /doc/refman/RefMan-oth.tex | |
| parent | e70165079e8defe490a568ece20a7029e4c1626e (diff) | |
| parent | 119d61453c6761f20b8862f47334bfb8fae0049e (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'doc/refman/RefMan-oth.tex')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 7c95e4d4af..aea2bae38d 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -1083,26 +1083,6 @@ perform a {\tt Ltac \ident\ := {\rm\sl convtactic}}. \SeeAlso sections \ref{Conversion-tactics} -\subsection{\tt Set Virtual Machine -\label{SetVirtualMachine} -\optindex{Virtual Machine}} - -This activates the bytecode-based conversion algorithm. - -\subsection{\tt Unset Virtual Machine -\optindex{Virtual Machine}} - -This deactivates the bytecode-based conversion algorithm. - -\subsection{\tt Test Virtual Machine -\optindex{Virtual Machine}} - -This tells if the bytecode-based conversion algorithm is -activated. The default behavior is to have the bytecode-based -conversion algorithm deactivated. - -\SeeAlso sections~\ref{vmcompute} and~\ref{vmoption}. - \section{Controlling the locality of commands} \subsection{{\tt Local}, {\tt Global} |