Documentation Whelp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9028 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 66 insertions, 0 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 35c55e07b..5ec2d77ca 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