From ef3245142c970c1407f10be03f0273d46d6819a9 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 4 Dec 2019 14:10:14 +0100
Subject: [PATCH] [WP/doc] Documents -wp-run-all-provers

---
 src/plugins/wp/doc/manual/wp_plugin.tex | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 3d0330f4f5b..82d7691f3e1 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -995,6 +995,9 @@ Support for \textsf{Why-3 IDE} is no longer provided.
   installing \textsf{Frama-C}.
   The option reads your \textsf{Why-3} configuration and prints the available
   provers with their \verb+-wp-prover <p>+ code names.
+\item[\tt -wp-(no)-run-all-provers] Run all specified provers on each goal not
+  proved by Qed. When a prover succeeds in proving the goal, the others are not
+  stopped. (default is: no).
 \item[\tt -wp-gen] only generates proof obligations, does not run provers.
   See option \texttt{-wp-out} to obtain the generated proof obligations.
 \item[\tt -wp-par <n>] limits the number of parallel process runs for
@@ -1241,7 +1244,7 @@ interactively or incrementally, it is often the case where most proof obligation
 from one \textsf{WP} execution to the other. To reduce this costs, a cache of prover results can be used
 and stored in your session.
 
-% The cache can only be used with \textsf{Why-3} provers, it does not work with native \textsf{Alt-Ergo} and \textsf{Coq} provers. 
+% The cache can only be used with \textsf{Why-3} provers, it does not work with native \textsf{Alt-Ergo} and \textsf{Coq} provers.
 There are different ways of using the cache, depending on your precise needs.
 The main option to control cache usage is \verb+-wp-cache+, documented below:
 
-- 
GitLab