diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 0090e3b22d88b94a02048cfcd9628bddd5a6e1cd..42a5e04927a0de38125052b85b77280c49df3ee2 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1442,6 +1442,8 @@ src/plugins/wp/ProverSearch.ml: CEA_WP
 src/plugins/wp/ProverSearch.mli: CEA_WP
 src/plugins/wp/ProverTask.ml: CEA_WP
 src/plugins/wp/ProverTask.mli: CEA_WP
+src/plugins/wp/ProverWhy3.mli: CEA_WP
+src/plugins/wp/ProverWhy3.ml: CEA_WP
 src/plugins/wp/REVISION: .ignore
 src/plugins/wp/RefUsage.ml: CEA_WP
 src/plugins/wp/RefUsage.mli: CEA_WP
@@ -1525,8 +1527,6 @@ src/plugins/wp/ctypes.ml: CEA_WP
 src/plugins/wp/ctypes.mli: CEA_WP
 src/plugins/wp/filter_axioms.ml: CEA_WP
 src/plugins/wp/filter_axioms.mli: CEA_WP
-src/plugins/wp/why3_api.mli: CEA_WP
-src/plugins/wp/why3_api.ml: CEA_WP
 src/plugins/wp/doc/MakeDoc: .ignore
 src/plugins/wp/doc/coqdoc/Makefile: .ignore
 src/plugins/wp/doc/coqdoc/coqdoc.sty: .ignore
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 900a4581d63d28278d7541395cf40b8eabb34355..cc19d6ae68d9ba547a44823fcb719bccd3b0e145 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -88,7 +88,7 @@ PLUGIN_CMO:= \
 	TacCongruence TacOverflow Auto \
 	ProofSession ProofScript ProofEngine \
 	ProverTask ProverErgo ProverCoq \
-	filter_axioms why3_api \
+	filter_axioms ProverWhy3 \
 	driver prover ProverSearch ProverScript \
 	Generator Factory \
 	calculus cfgDump cfgWP \
diff --git a/src/plugins/wp/why3_api.ml b/src/plugins/wp/ProverWhy3.ml
similarity index 99%
rename from src/plugins/wp/why3_api.ml
rename to src/plugins/wp/ProverWhy3.ml
index 1d4c70adb6379fd1630c89b060cfdb0c7adf4d44..83e0c580858007d53dbac44bff19edd3bf717fac 100644
--- a/src/plugins/wp/why3_api.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -608,7 +608,7 @@ module CLUSTERS = Model.Index
     (struct
       type key = Definitions.cluster
       type data = int * Why3.Theory.theory
-      let name = "Why3_api.CLUSTERS"
+      let name = "ProverWhy3.CLUSTERS"
       let compare = Definitions.cluster_compare
       let pretty = Definitions.pp_cluster
     end)
diff --git a/src/plugins/wp/why3_api.mli b/src/plugins/wp/ProverWhy3.mli
similarity index 100%
rename from src/plugins/wp/why3_api.mli
rename to src/plugins/wp/ProverWhy3.mli
diff --git a/src/plugins/wp/prover.ml b/src/plugins/wp/prover.ml
index 245225db0d92e716009a619601a7c4b34857c868..85b63a14b2b84270803e45dccbb3e8484ae01766 100644
--- a/src/plugins/wp/prover.ml
+++ b/src/plugins/wp/prover.ml
@@ -30,18 +30,15 @@ open Task
 open Wpo
 
 let dispatch ?(config=VCS.default) mode prover wpo =
-  let why3 prover =
-    Why3_api.prove
-      ~timeout:(VCS.get_timeout config)
-      ~steplimit:(VCS.get_stepout config)
-      ~prover wpo
-  in
   begin
     match prover with
-    | Why3 prover -> why3 prover
+    | Qed | Tactical -> Task.return VCS.no_result
     | NativeAltErgo -> ProverErgo.prove ~config ~mode wpo
     | NativeCoq -> ProverCoq.prove mode wpo
-    | Qed | Tactical -> Task.return VCS.no_result
+    | Why3 prover -> ProverWhy3.prove
+                       ~timeout:(VCS.get_timeout config)
+                       ~steplimit:(VCS.get_stepout config)
+                       ~prover wpo
   end
 
 let started ?start wpo =
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 04fc43af94d6f4c4a4bd7b64bc7345095ad11e4d..2a4a6c5f31c89de9db5affe7f55382a3d78e963f 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -837,7 +837,7 @@ let () = Cmdline.run_after_setting_files
        if Wp_parameters.has_dkey dkey_shell then
          Log.print_on_output pp_wp_parameters)
 
-let () = Cmdline.run_after_configuring_stage Why3_api.parse_why3_options
+let () = Cmdline.run_after_configuring_stage ProverWhy3.parse_why3_options
 
 let do_prover_detect () =
   if not !Config.is_gui && Wp_parameters.Detect.get () then