diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/faq/FAQ.tex | 9 |
1 files 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?} |