diff options
| -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 1c28063e6..647a151d7 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}?} |