From d069cd2ddc93daa088ea621b93cf65df6f7a8b8d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 2 Nov 2020 14:31:23 +0100
Subject: [PATCH] Apply suggestion to src/plugins/wp/doc/manual/wp_plugin.tex

---
 src/plugins/wp/doc/manual/wp_plugin.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index bd425850a74..21548b088c4 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -901,7 +901,7 @@ int caller(int (*fp)(int)){
 }
 \end{lstlisting}
 
-generates two goals for \verb+POST+, one for call to \verb+f1+ and
+These annotations split post-conditions to the dynamic call into two sub-goals: one for call to \verb+f1+ and
 a second for the call to \verb+f2+. A last goal is generated at the call
 site: one must prove that \verb+fp+ is either \verb+f1+ or \verb+f2+.
 
-- 
GitLab