1 files changed, 99 insertions, 1 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index e92cde74..1d2057a9 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -334,6 +334,72 @@ Locate I.Dont.Exist.
 
 \SeeAlso Section \ref{LocateSymbol}
 
+\subsection{The {\sc Whelp} searching tool
+\label{Whelp}}
+
+{\sc Whelp} is an experimental searching and browsing tool for the
+whole {\Coq} library and the whole set of {\Coq} user contributions.
+{\sc Whelp} requires a browser to work. {\sc Whelp} has been developed
+at the University of Bologna as part of the HELM\footnote{Hypertextual
+Electronic Library of Mathematics} and MoWGLI\footnote{Mathematics on
+the Web, Get it by Logics and Interfaces} projects.  It can be invoked
+directly from the {\Coq} toplevel or from {\CoqIDE}, assuming a
+graphical environment is also running. The browser to use can be
+selected by setting the environment variable {\tt
+COQREMOTEBROWSER}. If not explicitly set, it defaults to
+\verb!netscape -remote "OpenURL(%s)"!  or
+\verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the
+underlying operating system (in the command, the string \verb!%s!
+serves as metavariable for the url to open).
+
+The {\sc Whelp} commands are:
+
+\subsubsection{\tt Whelp Locate "{\sl reg\_expr}".
+\comindex{Whelp Locate}}
+
+This command opens a browser window and displays the result of seeking
+for all names that match the regular expression {\sl reg\_expr} in the
+{\Coq} library and user contributions. The regular expression can
+contain the special operators are * and ? that respectively stand for
+an arbitrary substring and for exactly one character.
+
+\variant {\tt Whelp Locate {\ident}.}\\
+This is equivalent to {\tt Whelp Locate "{\ident}"}.
+
+\subsubsection{\tt Whelp Match {\pattern}.
+\comindex{Whelp Match}}
+
+This command opens a browser window and displays the result of seeking
+for all statements that match the pattern {\pattern}. Holes in the
+pattern are represented by the wildcard character ``\_''.
+
+\subsubsection{\tt Whelp Instance {\pattern}.}
+\comindex{Whelp Instance}
+
+This command opens a browser window and displays the result of seeking
+for all statements that are instances of the pattern {\pattern}. The
+pattern is here assumed to be an universally quantified expression.
+
+\subsubsection{\tt Whelp Elim {\qualid}.}
+\comindex{Whelp Elim}
+
+This command opens a browser window and displays the result of seeking
+for all statements that have the ``form'' of an elimination scheme
+over the type denoted by {\qualid}.
+
+\subsubsection{\tt Whelp Hint {\term}.}
+\comindex{Whelp Hint}
+
+This command opens a browser window and displays the result of seeking
+for all statements that can be instantiated so that to prove the
+statement {\term}.
+
+\variant {\tt Whelp Hint.}\\ This is equivalent to {\tt Whelp Hint
+{\sl goal}} where {\sl goal} is the current goal to prove. Notice that
+{\Coq} does not send the local environment of definitions to the {\sc
+Whelp} tool so that it only works on requests strictly based on, only,
+definitions of the standard library and user contributions.
+
 \section{Loading files}
 
 \Coq\ offers the possibility of loading different
@@ -765,7 +831,39 @@ This command displays the current nesting depth used for display.
 %\subsection{\tt Abstraction ...}
 %Not yet documented.
 
-% $Id: RefMan-oth.tex 8606 2006-02-23 13:58:10Z herbelin $ 
+\section{Controlling the conversion algorithm}
+
+{\Coq} comes with two algorithms to check the convertibility of types
+(see section~\ref{convertibility}). The first algorithm lazily
+compares applicative terms while the other is a brute-force but efficient
+algorithm that first normalizes the terms before comparing them.  The
+second algorithm is based on a bytecode representation of terms
+similar to the bytecode representation used in the ZINC virtual
+machine~\cite{Leroy90}. It is specially useful for intensive
+computation of algebraic values, such as numbers, and for reflexion-based
+tactics.
+
+\subsection{\tt Set Virtual Machine
+\label{SetVirtualMachine}
+\comindex{Set Virtual Machine}}
+
+This activates the bytecode-based conversion algorithm.
+
+\subsection{\tt Unset Virtual Machine
+\comindex{Unset Virtual Machine}}
+
+This deactivates the bytecode-based conversion algorithm.
+
+\subsection{\tt Test Virtual Machine
+\comindex{Test 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}.
+
+% $Id: RefMan-oth.tex 9044 2006-07-12 13:22:17Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex