diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index b89ca18abd9f3e48bdb709034e17c7ec072b388b..8b30530ca66b4791e2f4f806ca2ba6dacd8f5f17 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -378,6 +378,12 @@ Finally, when the user select a arithmetic comparison over $a$ and $b$, the tact
 \Delta,a>b&\models G
 \end{array}} \]
 
+\paragraph{Validity} Unfold validity and range definitions\\
+The user selects a validity expression (\lstinline{valid_rd},
+\lstinline{valid_rw}, \lstinline{invalid} or \lstinline{included}).
+The expression is unfolded to a \textsf{Qed} term.
+
+
 \subsubsection{Over integers}
 
 \paragraph{BitRange} Range of logical bitwise operators \\