diff --git a/INSTALL.md b/INSTALL.md
index 7c8de3fe75796bfd005087a7fe8a860bbd1f2abc..fd85b7bfcb472ec6f8fa61e62605e95cf60bc646 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -82,7 +82,7 @@ Frama-C 19 (Potassium):
 - lablgtk.2.18.5 | lablgtk3.3.0.beta5 + lablgtk3-sourceview3.3.0.beta5
 - mlgmpidl.1.2.9 (optional)
 - ocamlgraph.1.8.8
-- why3.1.2.0 (optional)
+- why3.1.2.0
 - why3-coq.1.2.0 (optional)
 - yojson.1.4.1
 - zarith.1.7
@@ -225,7 +225,6 @@ We recommend to rely on it for the installation of Frama-C.
 
     ```shell
     brew install graphviz
-    opam install why3
     ```
 
 5. Install *optional* dependencies for Frama-C/WP:
diff --git a/opam/opam b/opam/opam
index 3b6424cf61d919a5f75ebeb120dd05eb2d6a6d04..b430aac839e8b4c64f439c3731ac05312133ae68 100644
--- a/opam/opam
+++ b/opam/opam
@@ -97,6 +97,7 @@ depends: [
   ( "alt-ergo-free" | "alt-ergo" )
   "conf-graphviz" { post }
   "yojson"
+  "why3"
 ]
 
 depopts: [
@@ -104,7 +105,6 @@ depopts: [
   # Coq: because .vo would would not be loadable by another version of Coq
   # libraries: because we use dynamic linking
   "coq"
-  "why3"
   "why3-coq"
   "mlgmpidl"
   "apron"
@@ -121,8 +121,6 @@ conflicts: [
 ]
 
 messages: [
-  "Why3 can be used by the WP plug-in for running additional automatic solvers"
-    {!why3:installed}
   "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"