diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index bd425850a748e85a33747a975511d092221e1083..21548b088c460007bc8fb9b9bb3b71d8f1f65e46 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+.