[opam] fix for wp

 - deprecation messages for alt[gr]-ergo and coq[ide]
 - require why3 >= 1.2.0 (includes conflicts with why3-base)
 - no more need for why3-coq

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}
 ]