[wp/doc] Indicates that interactive provers other than Coq have not been tested so far

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;