heveaifie

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

1 files changed, 13 insertions, 13 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 1fb5a81139..55299d90b2 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -278,13 +278,13 @@ todo christine compilo lustre ?
 \Question{Where can I find documentation about \Coq ?} 
 All the documentation about \Coq, from the reference manual~\cite{Coq:manual} to
 friendly tutorials~\cite{Coq:Tutorial} and documentation of the standard library, is available online at 
-\url{http://coq.inria.fr/coq/doc-eng.html}.
+\ahref{http://coq.inria.fr/coq/doc-eng.html}{\url{http://coq.inria.fr/coq/doc-eng.html}}.
 All these documents are viewable either in browsable HTML, or as
 downloadable postscripts.
 
 \Question{Where can I find this FAQ on the web ?}
 
-This FAQ is available online at \url{http://coq.inria.fr/faq.html}.
+This FAQ is available online at \ahref{http://coq.inria.fr/faq.html}{\url{http://coq.inria.fr/faq.html}}.
 
 \Question{How can I submit suggestions / improvements / additions for this FAQ?}
 
@@ -295,17 +295,17 @@ sections that are missing). Please send contributions to \texttt{Florent.Kirchne
 The main \Coq mailing list is \url{coq-club@coq.inria.fr}, which
 broadcasts questions and suggestions about the implementation, the
 logical formalism or proof developments. See
-\url{http://coq.inria.fr/mailman/listinfo/coq-club} for
+\ahref{http://coq.inria.fr/mailman/listinfo/coq-club}{\url{http://coq.inria.fr/mailman/listinfo/coq-club}} for
 subsription. For bugs reports see question \ref{coqbug}.
 
 \Question{Where can I find an archive of the list?}
 The archives of the \Coq mailing list are available at
-\url{http://coq.inria.fr/pipermail/coq-club}.
+\ahref{http://coq.inria.fr/pipermail/coq-club}{\url{http://coq.inria.fr/pipermail/coq-club}}.
 
 
 \Question{How can I be kept informed of new releases of \Coq ?}
 
-New versions of \Coq are announced on the coq-club mailing list. If you only want to receive information about new releases, you can subscribe to \Coq on \url{http://freshmeat.net/projects/coq/}.
+New versions of \Coq are announced on the coq-club mailing list. If you only want to receive information about new releases, you can subscribe to \Coq on \ahref{http://freshmeat.net/projects/coq/}{\url{http://freshmeat.net/projects/coq/}}.
 
 
 \Question{Is there any book about \Coq ?}
@@ -321,14 +321,14 @@ development of zero-default software.''
 \Question{Where can I find some \Coq examples ?} 
 
 There are examples in the manual~\cite{Coq:manual} and in the
-Coq'Art~\cite{Coq:coqart} exercises \url{http://www.labri.fr/Perso/~casteran/CoqArt/index.html}.
+Coq'Art~\cite{Coq:coqart} exercises \ahref{http://www.labri.fr/Perso/~casteran/CoqArt/index.html}{\url{http://www.labri.fr/Perso/~casteran/CoqArt/index.html}}.
 You can also find large developments using
 \Coq in the \Coq user contributions :
-\url{http://coq.inria.fr/distrib-eng.html}.
+\ahref{http://coq.inria.fr/distrib-eng.html}{\url{http://coq.inria.fr/distrib-eng.html}}.
 
 \Question{How can I report a bug ?}\label{coqbug}
 
-You can use the web interface at \url{http://coq.inria.fr/bin/coq-bugs}.
+You can use the web interface at \ahref{http://coq.inria.fr/bin/coq-bugs}{\url{http://coq.inria.fr/bin/coq-bugs}}.
 
 
 
@@ -341,8 +341,8 @@ It is distributed under the GNU Lesser General License (LGPL).
 
 \Question{Where can I find the sources of \Coq ?}
 The sources of \Coq can be found online in the tar.gz'ed packages
-(\url{http://coq.inria.fr/distrib-eng.html}). Development sources can
-be accessed via anonymous CVS : \url{http://coqcvs.inria.fr/}
+(\ahref{http://coq.inria.fr/distrib-eng.html}{\url{http://coq.inria.fr/distrib-eng.html}}). Development sources can
+be accessed via anonymous CVS : \ahref{http://coqcvs.inria.fr/}{\url{http://coqcvs.inria.fr/}}
 
 \Question{On which platform \Coq is available ?}
 Compiled binaries are available for Linux, MacOS X, Solaris, and
@@ -1144,7 +1144,7 @@ to abstract the appropriate terms.
 
 PS: Notice for people that are interested in proof rendering that \assert
 and \pose (and \cut) are not rendered the same as \generalize (see the
-HELM experimental rendering tool at \url{http://mowgli.cs.unibo.it}, link
+HELM experimental rendering tool at \ahref{http://mowgli.cs.unibo.it}{\url{http://mowgli.cs.unibo.it}}, link
 HELM, link COQ Online). Indeed \generalize builds a beta-expanded term
 while \assert, \pose and \cut uses a let-in.
 
@@ -1250,7 +1250,7 @@ Use the \inversion tactic.
 
 \Question{How can I prove that 2 terms in an inductive set are equal? Or different?}
 
-Have a look at "decide equality" and "discriminate" in the \ahref{\refman}{Reference Manual}.
+Have a look at "decide equality" and "discriminate" in the \ahref{http://coq.inria.fr/doc/main.html}{Reference Manual}.
 
 \Question{Why is the proof of \coqtt{0+n=n} on natural numbers
 trivial but the proof of \coqtt{n+0=n} is not?}
@@ -1799,7 +1799,7 @@ pretty simple notations.
 \item First solution : type \verb#<CONTROL><SHIFT>2200# to enter a forall in the script widow. 
 	2200 is the hexadecimal code for forall in unicode charts and is encoded as 	
 	in UTF-8.
-	2203 is for exists. See \url{http://www.unicode.org} for more codes.
+	2203 is for exists. See \ahref{http://www.unicode.org}{\url{http://www.unicode.org}} for more codes.
 \item Second solution : rebind \verb#<AltGr>a# to forall and \verb#<AltGr>e# to exists. 
 	Under X11, you need to use something like
 \begin{verbatim}