diff --git a/INSTALL.md b/INSTALL.md
index bebc38796e2ac884fce5cf7f1651053629a7d9d6..4552589954cfa5be743bab57be23aa9071a225ce 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -7,7 +7,7 @@
         - [Installing Frama-C from opam repository](#installing-frama-c-from-opam-repository)
         - [Installing Custom Versions of Frama-C](#installing-custom-versions-of-frama-c)
         - [Installing Frama-C on Windows via WSL](#installing-frama-c-on-windows-via-wsl)
-        - [Installing Frama-C on macOS](#installing-frama-c-on-macos)
+        - [Installing Frama-C on macOS](#installing-frama-c-on-mac-os)
     - [Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)](#installing-frama-c-via-your-linux-distribution-debianubuntufedora)
     - [Compiling from source](#compiling-from-source)
         - [Quick Start](#quick-start)
@@ -70,22 +70,38 @@ so that we can add it to the Frama-C `depext` package.
     # install Frama-C
     opam install frama-c
 
+### Configuring provers for Frama-C/WP
+
+Frama-C/WP uses the [Why3](http://why3.lri.fr/) platform to run external provers for proving ACSL annotations.
+The Why3 platform and the Alt-Ergo prover are automatically installed _via_ opam
+when installing Frama-C.
+
+Other recommended, efficient provers are CVC4 and Z3.
+They can be used as replacement or combined with Alt-Ergo.
+Actually, you can use any prover supported by Why3 in combination with Frama-C/WP.
+
+Most provers are available on all platforms. After their installation,
+Why3 must be configured to make them available for Frama-C/WP:
+
+    ```shell
+    why3 config --detect
+    ```
+
 ### Known working configuration
 
 The following set of packages is known to be a working configuration for
 Frama-C 19 (Potassium):
 
 - OCaml 4.05.0
-- alt-ergo-free.2.0.0 (optional)
+- ocamlfind.1.8.0
 - apron.20160125 (optional)
-- coq.8.9.0 (optional)
-- lablgtk.2.18.5 | lablgtk3.3.0.beta5 + lablgtk3-sourceview3.3.0.beta5
-- mlgmpidl.1.2.9 (optional)
+- lablgtk.2.18.8 | lablgtk3.3.0.beta6 + lablgtk3-sourceview3.3.0.beta6
+- mlgmpidl.1.2.11 (optional)
 - ocamlgraph.1.8.8
 - why3.1.2.0
-- why3-coq.1.2.0 (optional)
-- yojson.1.4.1
-- zarith.1.7
+- alt-ergo.2.0.0 (for wp, optional)
+- yojson.1.7.0
+- zarith.1.9.1
 
 ### Installing Custom Versions of Frama-C
 
@@ -197,7 +213,7 @@ frama-c-gui
 
 [opam](https://opam.ocaml.org) works perfectly on macOS via
 [Homebrew](https://brew.sh).
-We recommend to rely on it for the installation of Frama-C.
+We highly recommend to rely on it for the installation of Frama-C.
 
 1. Install *required* general macOS tools for OCaml:
 
@@ -206,7 +222,7 @@ We recommend to rely on it for the installation of Frama-C.
     ```
 
    Do not forget to `opam init` and ``eval `opam config env` `` for a proper
-   opam installation (if not already done before on your machine).
+   opam installation (if not already done before).
 
 2. Set up a compatible OCaml version (replace `<version>` with the version
    indicated in the 'recommended working configuration' section):
@@ -221,31 +237,25 @@ We recommend to rely on it for the installation of Frama-C.
     brew install gmp gtk+ gtksourceview libgnomecanvas
     ```
 
-4. Install *recommended* dependencies for Frama-C:
+    The graphical libraries require additional manual configuration of your
+    bash profile. Consult this [issue](https://github.com/ocaml/opam-repository/issues/13709) on opam
+    for details. A known working configuration is:
 
     ```shell
-    brew install graphviz
+    export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig:/usr/local/opt/libxml2/lib/pkgconfig:/usr/local/lib/pkgconfig
     ```
 
-5. Install *optional* dependencies for Frama-C/WP:
+4. Install *recommended* dependencies for Frama-C:
 
     ```shell
-    opam install coq coqide why3-coq
+    brew install graphviz
     ```
 
-6. Install Frama-C:
+5. Install Frama-C:
 
     ```shell
     opam install frama-c
     ```
-    **Note:** for some packages, Homebrew may emit *caveats* about the
-              necessity of manually setting environment variables,
-              e.g. for `libffi`.
-              If installation of some opam package fails, the error message
-              should hopefully indicate which packages are causing it.
-              Reinstalling these Homebrew packages can provide details and
-              help solve the issue.
-
 
 ## Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)
 
diff --git a/opam/opam b/opam/opam
index 83422183701882cda0474b21e9be95610e1769b7..05aa26d252a1ab3682196fe1963c2c2e6b9878a7 100644
--- a/opam/opam
+++ b/opam/opam
@@ -97,7 +97,7 @@ depends: [
   ( "alt-ergo-free" | "alt-ergo" )
   "conf-graphviz" { post }
   "yojson"
-  "why3"
+  "why3" { >= "1.2.0" }
 ]
 
 depopts: [
@@ -105,14 +105,11 @@ depopts: [
   # Coq: because .vo would would not be loadable by another version of Coq
   # libraries: because we use dynamic linking
   "coq"
-  "why3-coq"
   "mlgmpidl"
   "apron"
 ]
 
 conflicts: [
-  "why3-base" #for WP plug-in
-  "why3" { < "1.2.0" } #for WP plug-in
   "lablgtk" { < "2.18.2" } #for ocaml >= 4.02.1
   "frama-c-e-acsl" #avoid mixing old releases of E-ACSL, it is already
                    #distributed with this version of Frama-C
@@ -121,12 +118,8 @@ conflicts: [
 ]
 
 messages: [
-  "Coq can be used with the WP plug-in for proving interactively proof obligations"
-    {!coq:installed}
-  "Alt-Ergo Graphical Interface can be used by the WP plug-in"
-    {!altgr-ergo:installed & alt-ergo <= "1.30"}
-  "Note: the package altgr-ergo could prevent the installation of newer versions of Alt-Ergo"
-    {!altgr-ergo:installed & alt-ergo <= "1.30" & ocaml >= "4.04.0"}
-  "Note: the installed package altgr-ergo could prevent the installation of newer versions of Alt-Ergo"
-    {altgr-ergo:installed & ocaml >= "4.04.0"}
+  "The Frama-C/Wp now uses Why-3 for all provers (Cf. deprecated -wp-prover native:alt-ergo)"
+  {alt-ergo:installed}
+  "The Frama-C/Wp native support for Coq is now deprecated (use TIP or Why-3 instead)."
+  {coq:installed}
 ]
diff --git a/src/plugins/wp/share/Makefile.resources b/src/plugins/wp/share/Makefile.resources
index 4c153ff60070b9b23a2ad5e5833375629a4f1f2e..17399b03db40b234f061ebfec038995ea45d12c7 100644
--- a/src/plugins/wp/share/Makefile.resources
+++ b/src/plugins/wp/share/Makefile.resources
@@ -27,7 +27,6 @@
 ## Used in share/why3
 
 WHY3_LIBS_CEA:=	\
- ArcTrigo.mlw   \
  cbits.mlw 	\
  cint.mlw 	\
  cfloat.mlw 	\
diff --git a/src/plugins/wp/share/ergo/Cbits.mlw b/src/plugins/wp/share/ergo/Cbits.mlw
index 1bf6749cffed1c9e2e168e513d1960e72b6f64e5..4b2b2d6ed430f12ce4b1c5e3ee9a1380be4a3f7e 100644
--- a/src/plugins/wp/share/ergo/Cbits.mlw
+++ b/src/plugins/wp/share/ergo/Cbits.mlw
@@ -27,14 +27,12 @@
 (** The theory bool_Bool_ must be appended to this file*)
 (** The theory int_Int_ must be appended to this file*)
 (** The theory int_Abs_ must be appended to this file*)
-(** The theory int_EuclideanDivision_ must be appended to this file*)
 (** The theory int_ComputerDivision_ must be appended to this file*)
 (** The theory real_Real_ must be appended to this file*)
 (** The theory real_RealInfix_ must be appended to this file*)
 (** The theory real_FromInt_ must be appended to this file*)
-(** The theory for_drivers_ComputerOfEuclideanDivision_ must be appended to this file*)
 (** The theory Cint_ must be appended to this file*)
-<<<<<<< HEAD
+
 logic bit_testb : int, int -> bool
 
 logic bit_test : int, int -> prop
@@ -51,8 +49,6 @@ logic lsl : int, int -> int
 
 logic lsr : int, int -> int
 
-||||||| merged common ancestors
-=======
 axiom lnot_bool : (lnot(0) = (-1))
 
 axiom lnot_bool1 : (lnot((-1)) = 0)
@@ -87,7 +83,6 @@ axiom lxor_0 : (forall x:int [lxor(0, x)]. (lxor(0, x) = x))
 
 axiom lxor_0bis : (forall x:int [lxor(x, 0)]. (lxor(x, 0) = x))
 
->>>>>>> origin/master
 axiom bit_test_def :
   (forall x:int. forall k:int [bit_testb(x, k)]. ((bit_testb(x, k) = true) ->
   bit_test(x, k)))
@@ -536,4 +531,3 @@ axiom lor_addition :
 axiom lxor_addition :
   (forall x:int. forall y:int [land(x, y), lxor(x, y)]. ((land(x, y) = 0) ->
   ((x + y) = lxor(x, y))))
-
diff --git a/src/plugins/wp/share/ergo/Qed.mlw b/src/plugins/wp/share/ergo/Qed.mlw
index 0537e4c35cbdb14341fcfade5481df37a862b5b0..eeb3d92f8822c9f0c0e116425e7e9c457119cfca 100644
--- a/src/plugins/wp/share/ergo/Qed.mlw
+++ b/src/plugins/wp/share/ergo/Qed.mlw
@@ -26,12 +26,10 @@
 (** The theory bool_Bool_ must be appended to this file*)
 (** The theory int_Int_ must be appended to this file*)
 (** The theory int_Abs_ must be appended to this file*)
-(** The theory int_EuclideanDivision_ must be appended to this file*)
 (** The theory int_ComputerDivision_ must be appended to this file*)
 (** The theory real_Real_ must be appended to this file*)
 (** The theory real_RealInfix_ must be appended to this file*)
 (** The theory real_FromInt_ must be appended to this file*)
-(** The theory for_drivers_ComputerOfEuclideanDivision_ must be appended to this file*)
 logic match_bool : bool, 'a, 'a -> 'a
 
 axiom match_bool1 :
diff --git a/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw b/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw
index ab250caabbfa9ce388e6699ec584ccd4e0fd172b..4fca9c6c375416d431f1e8a4491f37f58da2b61f 100644
--- a/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw
+++ b/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw
@@ -17,8 +17,8 @@
 (** The theory Bool_ must be appended to this file*)
 (** The theory int_Int_ must be appended to this file*)
 (** The theory int_Abs_ must be appended to this file*)
-(** The theory int_EuclideanDivision_ must be appended to this file*)
 (** The theory int_ComputerDivision_ must be appended to this file*)
+
 axiom cdiv_cases :
   (forall n:int. forall d:int [div(n, d)]. ((0 <= n) -> ((0 <  d) -> (div(n,
   d) = (n / d)))))
@@ -50,4 +50,3 @@ axiom cmod_cases2 :
 axiom cmod_cases3 :
   (forall n:int. forall d:int [mod(n, d)]. ((n <= 0) -> ((d <  0) -> (mod(n,
   d) = (-((-n) % (-d)))))))
-
diff --git a/src/plugins/wp/share/ergo/int.EuclideanDivision.mlw b/src/plugins/wp/share/ergo/int.EuclideanDivision.mlw
deleted file mode 100644
index 7390354ffaa31e89b8924bf338a7840b799894f5..0000000000000000000000000000000000000000
--- a/src/plugins/wp/share/ergo/int.EuclideanDivision.mlw
+++ /dev/null
@@ -1,5 +0,0 @@
-(* this is the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** The theory BuiltIn_ must be appended to this file*)
-(** The theory Bool_ must be appended to this file*)
-(** The theory int_Int_ must be appended to this file*)
-(** The theory int_Abs_ must be appended to this file*)
diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index 271c470da94179003bfc30a861aa583070eb56e7..84cccb44f4c62d6bec8d985a038acc447e61238e 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -41,7 +41,6 @@ why3.import += "frama_c_wp.qed.Qed";
 altergo.file += "ergo/int.Int.mlw";
 altergo.file += "ergo/int.Abs.mlw";
 altergo.file += "ergo/int.ComputerDivision.mlw";
-altergo.file += "ergo/int.EuclideanDivision.mlw";
 altergo.file += "ergo/int.ComputerOfEuclideanDivision.mlw";
 altergo.file += "ergo/real.Real.mlw";
 altergo.file += "ergo/real.RealInfix.mlw";