diff options
| author | Pierre Letouzey | 2014-11-27 17:14:39 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-11-27 19:11:54 +0100 |
| commit | 8ff32fd0748b0d1d7bd0a7612e05c26236b65d48 (patch) | |
| tree | 85be6c7764add53575bd18bd3da423a041531438 | |
| parent | 7008576175028838d5d7ba899dbc44d04e2d23c1 (diff) | |
FAQ: fix some broken urls
| -rw-r--r-- | doc/faq/FAQ.tex | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 1c28063e68..647a151d70 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -37,7 +37,7 @@ % les macros d'amour \def\Coq{\textsc{Coq}} \def\Why{\textsc{Why}} -\def\Caduceus{\textsc{Caduceus}} +\def\Framac{\textsc{Frama-c}} \def\Krakatoa{\textsc{Krakatoa}} \def\Ltac{\textsc{Ltac}} \def\CoqIde{\textsc{CoqIde}} @@ -264,9 +264,9 @@ Eduardo Giménez' thesis~\cite{EGThese}. You can either extract a program from a proof by using the extraction mechanism or use dedicated tools, such as -\ahref{http://why.lri.fr}{\Why}, +\ahref{http://why3.lri.fr}{\Why}, \ahref{http://krakatoa.lri.fr}{\Krakatoa}, -\ahref{http://why.lri.fr/caduceus/index.en.html}{\Caduceus}, to prove +\ahref{http://frama-c.com}{\Framac}, to prove annotated programs written in other languages. %\Question{How many {\Coq} users are there?} @@ -371,7 +371,7 @@ downloadable postscripts. \Question{Where can I find this FAQ on the web?} -This FAQ is available online at \ahref{http://coq.inria.fr/doc/faq.html}{\url{http://coq.inria.fr/doc/faq.html}}. +This FAQ is available online at \ahref{http://coq.inria.fr/faq}{\url{http://coq.inria.fr/faq}}. \Question{How can I submit suggestions / improvements / additions for this FAQ?} @@ -382,12 +382,12 @@ sections that are missing). Please send contributions to Coq-Club. The main {\Coq} mailing list is \url{coq-club@inria.fr}, which broadcasts questions and suggestions about the implementation, the logical formalism or proof developments. See -\ahref{http://coq.inria.fr/mailman/listinfo/coq-club}{\url{http://sympa-roc.inria.fr/wws/info/coq-club}} for +\ahref{http://sympa.inria.fr/sympa/info/coq-club}{\url{http://sympa.inria.fr/sympa/info/coq-club}} for subscription. 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 -\ahref{http://pauillac.inria.fr/pipermail/coq-club}{\url{http://sympa-roc.inria.fr/wws/arc/coq-club}}. +\ahref{http://sympa.inria.fr/sympa/arc/coq-club}{\url{http://sympa.inria.fr/sympa/arc/coq-club}}. \Question{How can I be kept informed of new releases of {\Coq}?} |