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

[WP/Doc] Minor fixes

parent 6d71b9a5
No related branches found
No related tags found
No related merge requests found
......@@ -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.
%-----------------------------------------------------------------------------
......
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