diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 6d1d1a3a70cec1a9675a2c229b0f72e0ecacce18..40d9d63d4dbbbe2a2b8d52cdd48e586e158b999a 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -754,7 +754,7 @@ interface of the programmatic API.
     \texttt{@<category>} of properties.
     \\
     Recognized categories are: \texttt{@lemma}, \texttt{@requires}, \texttt{@assigns},
-    \texttt{@ensures}, \texttt{@exits},  \texttt{@assert},
+    \texttt{@ensures}, \texttt{@exits}, \texttt{@assert}, \texttt{@check},
     \texttt{@invariant}, \texttt{@variant}, \texttt{@breaks},
     \texttt{@continues}, \texttt{@returns}, \\
     \texttt{\mbox{@complete\_behaviors}}, \texttt{\mbox{@disjoint\_behaviors}}.