diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex index 403ea107b96337b5c46d3afccdb86b38b8d04426..c8b8b89130d3bc301d2b89a9aa88880de8598c85 100644 --- a/src/plugins/wp/doc/manual/wp_plugin.tex +++ b/src/plugins/wp/doc/manual/wp_plugin.tex @@ -34,7 +34,7 @@ The recommended versions for external provers are: \begin{tabular}{crlc} Prover & Versions & Download &\\ \hline - \textsf{Why3} & \verb|1.2.0| & + \textsf{Why3} & \verb|1.3.1| & \url{http://why3.lri.fr} & \cite{Why3}\\ \textsf{Alt-Ergo} & \verb|2.0.0| & \url{http://alt-ergo.ocamlpro.com} & \cite{AltErgo2006}\\ @@ -48,7 +48,7 @@ Other versions might be supported as well, typically, as far as we know: \begin{itemize} \item \textsf{Alt-Ergo} \verb+2.2.0+ and \verb+2.3.0+, although distributed under a non-commercial licence. % \item \textsf{Coq} \verb+8.7.2+ and \verb+8.8.2+, although proof scripts compatibility can be an issue. -\item \textsf{Why3} \verb+1.0.0+ and \verb+1.1.1+, although only \verb+1.2.0+ is provided with Coq support. +\item \textsf{Why3} \verb+1.3.1+. \end{itemize} Other provers, like \textsf{Coq}, \textsf{Gappa}, \textsf{Z3}, \textsf{CVC3},