From 85a870d3e8f3f26222245af4d0d2a54ccf52eeb8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 1 Oct 2011 09:12:15 +0000
Subject: Updating some links in the FAQ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14506 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/faq/FAQ.tex | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index e4d303e690..eddbb8d640 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -412,7 +412,7 @@ There are examples in the manual~\cite{Coq:manual} and in the
 Coq'Art~\cite{Coq:coqart} exercises \ahref{\url{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:
-\ahref{http://coq.inria.fr/contribs-eng.html}{\url{http://coq.inria.fr/contribs-eng.html}}.
+\ahref{http://coq.inria.fr/contribs}{\url{http://coq.inria.fr/contribs}}.
 
 \Question{How can I report a bug?}\label{coqbug}
 
@@ -665,9 +665,10 @@ where both excluded-middle and the axiom of description are valid (see
 file \vfile{\LogicClassicalDescription}{ClassicalDescription} for a
 proof that excluded-middle and description implies the double negation
 of excluded-middle in {\Set} and file {\tt Hurkens\_Set.v} from the
-user contribution {\tt Rocq/PARADOXES} for a proof that
-impredicativity of {\Set} implies the simple negation of
-excluded-middle in {\Set}).
+user contribution {\tt Paradoxes} at
+\ahref{http://coq.inria.fr/contribs}{\url{http://coq.inria.fr/contribs}}
+for a proof that impredicativity of {\Set} implies the simple negation
+of excluded-middle in {\Set}).
 
 \Question{Is {\Type} impredicative?}
 
-- 
cgit v1.2.3