From c734a8890603c2b01b80123df1af954622cbbcb7 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 17 Oct 2019 09:38:27 +0200
Subject: [PATCH] [WP/Doc] Minor fixes
---
src/plugins/wp/doc/manual/wp_intro.tex | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/doc/manual/wp_intro.tex b/src/plugins/wp/doc/manual/wp_intro.tex
index 3c98c0ef428..87cf5ca2b52 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.
%-----------------------------------------------------------------------------
--
GitLab