diff --git a/src/plugins/wp/doc/manual/wp_intro.tex b/src/plugins/wp/doc/manual/wp_intro.tex index 3c98c0ef42836166a707d982ebe318e03a4e92e4..87cf5ca2b52496de946fe09bdd591d0ce4e17656 100644 --- a/src/plugins/wp/doc/manual/wp_intro.tex +++ b/src/plugins/wp/doc/manual/wp_intro.tex @@ -55,11 +55,11 @@ The \textsf{WP} plug-in is distributed with the \textsf{Frama-C} platform. However, it also requires the \textsf{Why-3} platform and you should install at least one external prover in order to fulfill proof obligations. An easy choice is to install the -\textsf{Alt-Ergo} theorem prover developed at -\textsc{inria}\footnote{\textsf{Alt-Ergo}: +\textsf{Alt-Ergo} theorem prover originally developed at +\textsc{inria} and now by \textsc{OcamlPro}\footnote{\textsf{Alt-Ergo}: \url{https://alt-ergo.ocamlpro.com/}}. When using the \textsf{Opam} package manager, these tools are automatically installed with \textsf{Frama-C}. -See section~\ref{wp-install-provers} for installing other provers. +See the documentation of \textsf{Why-3} to install other provers. %-----------------------------------------------------------------------------