1 files changed, 0 insertions, 81 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 4547c7fd89..32f94abf7a 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -490,87 +490,6 @@ 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!firefox -remote \"OpenURL(%s,new-tab)\" || firefox %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 Whelp tool relies on a dedicated Whelp server and on
-another server called Getter that retrieves formal documents. The default Whelp
-server name can be obtained using the command {\tt Test Whelp Server} and the
-default Getter can be obtained using the command: {\tt Test Whelp Getter}. The
-Whelp server name can be changed using the command:
-
-\smallskip
-\noindent {\tt Set Whelp Server {\str}}.\\
-where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58080}).
-\optindex{Whelp Server}
-\smallskip
-
-\noindent The Getter can be changed using the command:
-\smallskip
-
-\noindent {\tt Set Whelp Getter {\str}}.\\
-where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58081}).  
-\optindex{Whelp Getter}
-
-\bigskip
-
-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}.]{\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}.]{\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}.]{\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