diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 39ba32bc5e3dd813214d506c4d40dbd300b79720..baabcb0c126a097e691c2abfbb2b0f1457321b4e 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -995,7 +995,8 @@ See \texttt{-wp-interactive <mode>} option for details.
   For each goal, the first decision procedure that succeeds cancels the
   other attempts.
 \item[\tt -wp-interactive <mode>] selects the interaction mode with
-  interactive provers such as Coq. Five modes are available:
+  interactive provers such as Coq (while it could work for other interactive
+  provers, it has not been tested so far). Five modes are available:
   \begin{itemize}
   \item \texttt{"batch"} mode only check existing scripts (the default);
   \item \texttt{"update"} mode update the script and then checks it;