[opam] add why3 as mandatory dependence

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:

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"