[WP/Doc] Removes native support of Alt-Ergo/Coq

src/plugins/wp/doc/manual/wp_intro.tex

@@ -25,7 +25,7 @@ heterogeneous casts, are involved. Moreover, \textsf{Jessie}
 operates by compiling the \textsf{C} program to \textsf{Why}, a
 solution that prevents the user from combining \textit{weakest
   precondition calculus} with other techniques, such as the
-\textsf{Value} analysis plug-in.
+\textsf{Eva} analysis plug-in.
 
 The \textsf{WP} plug-in has been designed with cooperation in
 mind. That is, you may use \textsf{WP} for proving some annotations of
@@ -51,12 +51,14 @@ precondition engine implemented in the \textsf{WP} plug-in.
 %-----------------------------------------------------------------------------
 
 The \textsf{WP} plug-in is distributed with the \textsf{Frama-C}
-platform. However, you should install at least one external prover in
+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}:
-  \url{http://alt-ergo.lri.fr}}.  See section~\ref{wp-install-provers}
-for installing other provers.
+  \url{http://alt-ergo.lri.fr}}. 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.
 
 
 %-----------------------------------------------------------------------------
@@ -94,7 +96,7 @@ should be valid.
 By default, the \textsf{WP} plug-in does not generate any proof obligation
 for verifying the absence of runtime errors in your code. Absence of runtime errors
 can be proved with other techniques, for instance by running
-the \textsf{Value} plug-in, or by generating all the necessary annotations
+the \textsf{Eva} plug-in, or by generating all the necessary annotations
 with the \textsf{RTE} plug-in.
 
 The simple contract for the \texttt{swap} function above is not strong enough to
@@ -196,8 +198,8 @@ Regarding runtime errors, the proof obligations generated by
 \textsf{WP} assume your program never raises any of them. As
 illustrated in the short tutorial example of
 section~\ref{wp-tutorial}, you should enforce the absence of runtime
-errors on your own, for instance by running the \emph{value analysis}
-plug-in or the \emph{rte generation} one and proving the generated assertions.
+errors on your own, for instance by running the \textsf{Eva}
+plug-in or the \textsf{RTE} one and proving the generated assertions.
 
 %-----------------------------------------------------------------------------
 \section{Memory Models}
@@ -361,5 +363,5 @@ For tackling this complexity, the \textsf{WP} plug-in relies on several
 \paragraph{Remark:} with all models, there are conditions to meet for WP
 proofs to be correct. Depending on the model used and the kernel options, those conditions
 may change. WP do not generate proof obligations for runtime errors on its own. Instead, it can
-discharge the annotations generated by the Value analysis plug-in, or by the RTE plug-in.
+discharge the annotations generated by the \textsf{Eva} analysis plug-in, or by the \textsf{RTE} plug-in.
 Consider also using \textsf{-wp-rte} option.