Skip to content
Snippets Groups Projects
Commit f631a029 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp/doc] Fixes Why3 version

parent c384486c
No related branches found
No related tags found
No related merge requests found
......@@ -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},
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment