Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.

1 files changed, 8 insertions, 5 deletions

diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 7227f4b7b..4ebb484e7 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -17,10 +17,11 @@ The \Coq\ library is structured into two parts:
 
 In addition, user-provided libraries or developments are provided by
 \Coq\ users' community. These libraries and developments are available
-for download at \texttt{http://coq.inria.fr} (see
+for download at \url{http://coq.inria.fr} (see
 Section~\ref{Contributions}).
 
-The chapter briefly reviews the \Coq\ libraries.
+The chapter briefly reviews the \Coq\ libraries whose contents can
+also be browsed at \url{http://coq.inria.fr/stdlib}.
 
 \section[The basic library]{The basic library\label{Prelude}}
 
@@ -799,7 +800,9 @@ At the end, it defines data-types at the {\Type} level.
 \subsection{Tactics}
 
 A few tactics defined at the user level are provided in the initial
-state\footnote{This is in module {\tt Tactics.v}}.
+state\footnote{This is in module {\tt Tactics.v}}. They are listed at
+\url{http://coq.inria.fr/stdlib} (paragraph {\tt Init}, link {\tt
+  Tactics}).
 
 \section{The standard library}
 
@@ -842,7 +845,7 @@ Chapter~\ref{Other-commands}).
 The different modules of the \Coq\ standard library are described in the
 additional document \verb!Library.dvi!. They are also accessible on the WWW
 through the \Coq\ homepage
-\footnote{\texttt{http://coq.inria.fr}}.
+\footnote{\url{http://coq.inria.fr}}.
 
 \subsection[Notations for integer arithmetics]{Notations for integer arithmetics\index{Arithmetical notations}}
 
@@ -1035,7 +1038,7 @@ intros; split_Rmult.
 
 \end{itemize}
 
-All this tactics has been written with the tactic language Ltac
+These tactics has been written with the tactic language Ltac
 described in Chapter~\ref{TacticLanguage}.
 
 \begin{coq_eval}