1 files changed, 5 insertions, 11 deletions
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 24eb3d1123..99c25d0568 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -882,8 +882,8 @@ Notation & Interpretation & Precedence & Associativity\\
 \verb!_ ^ _! & {\tt Zpower} &&\\
 \end{tabular}
 \end{center}
-\label{zarith-syntax}
 \caption{Definition of the scope for integer arithmetics ({\tt Z\_scope})}
+\label{zarith-syntax}
 \end{figure}
 
 Figure~\ref{zarith-syntax} shows the notations provided by {\tt
@@ -926,8 +926,8 @@ Notation & Interpretation \\
 \verb!_ * _! & {\tt mult} \\
 \end{tabular}
 \end{center}
-\label{nat-syntax}
 \caption{Definition of the scope for natural numbers ({\tt nat\_scope})}
+\label{nat-syntax}
 \end{figure}
 
 \subsection{Real numbers library}
@@ -1030,8 +1030,7 @@ intros; split_Rmult.
 \end{itemize}
 
 All this tactics has been written with the tactic language Ltac
-described in Chapter~\ref{TacticLanguage}.  More details are available
-in document \url{http://coq.inria.fr/~desmettr/Reals.ps}.
+described in Chapter~\ref{TacticLanguage}.
 
 \begin{coq_eval}
 Reset Initial.
@@ -1090,17 +1089,12 @@ Notation & Interpretation & Precedence & Associativity\\
 \label{Contributions}}
 
 Numerous users' contributions have been collected and are available at
-URL \url{coq.inria.fr/contribs/}.  On this web page, you have a list
+URL \url{http://coq.inria.fr/contribs/}.  On this web page, you have a list
 of all contributions with informations (author, institution, quick
 description, etc.) and the possibility to download them one by one.
-There is a small search engine to look for keywords in all
-contributions.  You will also find informations on how to submit a new
+You will also find informations on how to submit a new
 contribution.
 
-The users' contributions may also be obtained by anonymous FTP from site
-\verb:ftp.inria.fr:, in directory \verb:INRIA/coq/: and
-searchable on-line at \url{http://coq.inria.fr/contribs-eng.html}
-
 % $Id$ 
 
 %%% Local Variables: