From 238217bdcce6dd24a9bc3f0c7d5cc29bf0669fad Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 2 Oct 2020 13:15:10 +0200
Subject: [PATCH] [wp/doc] Indicates that interactive provers other than Coq
have not been tested so far
---
src/plugins/wp/doc/manual/wp_plugin.tex | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 39ba32bc5e3..baabcb0c126 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;
--
GitLab