Correction du bug #2214 + maj liens web

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

3 files changed, 7 insertions, 13 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index e33f9cce7b..f50c4fe1f0 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -282,7 +282,7 @@ declared in $E$, we write $c \in E$ and if $c:T$ or $c:=t:T$ is
 declared in $E$, we write $(c : T) \in E$.
 
 \paragraph[Typing rules.]{Typing rules.\label{Typing-rules}\index{Typing rules}}
-In the following, we assume $E$ is a valid environment wrt to
+In the following, we assume $E$ is a valid environment w.r.t.
 inductive definitions.  We define simultaneously two
 judgments.  The first one \WTEG{t}{T} means the term $t$ is well-typed
 and has type $T$ in the environment $E$ and context $\Gamma$.  The
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: 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ab8cfd07af..0b2c930b56 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -234,7 +234,7 @@ context\footnote{but it does not rename the hypothesis in the
 
 \begin{ErrMsgs}
 
-\item \errindex{{\ident$_2$} not found}
+\item \errindex{{\ident$_1$} not found}
 
 \item \errindexbis{{\ident$_2$} is already used}{is already used}