diff options
Diffstat (limited to 'doc/refman/RefMan-oth.tex')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 24 |
1 files changed, 2 insertions, 22 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index c444b5ae05..aea2bae38d 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -975,8 +975,8 @@ the constants {\qualid$_1$} {\ldots} {\qualid$_n$} in tactics using $\delta$-conversion (unfolding a constant is replacing it by its definition). -{\tt Opaque} has also on effect on the conversion algorithm of {\Coq}, -telling it to delay the unfolding of a constant as mush as possible when +{\tt Opaque} has also an effect on the conversion algorithm of {\Coq}, +telling it to delay the unfolding of a constant as much as possible when {\Coq} has to check the conversion (see Section~\ref{conv-rules}) of two distinct applied constants. @@ -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} |