diff --git a/opam/opam b/opam/opam
index a102e260f1917bf705f3806fcdaad692a90754f1..2ce4efbb5ddb8ec49da811f7047d633a86568380 100644
--- a/opam/opam
+++ b/opam/opam
@@ -104,11 +104,8 @@ run-test: [
   # available hardware to test them locally
 ]
 
+# Please keep depends and depopts sorted by package name
 depends: [
-  "ocaml" { >= "4.08.1" }
-  "ocamlgraph" { >= "1.8.8" }
-  "ocamlfind" # needed beyond build stage, used by -load-module
-  "zarith"
   "conf-autoconf" { build }
   ( ( "lablgtk" { >= "2.18.8" } & "conf-gnomecanvas" & "conf-gtksourceview"
       & ("ocamlgraph" { < "2.0" } | "ocamlgraph_gtk" ))
@@ -116,21 +113,25 @@ depends: [
         & "lablgtk3-sourceview3" & "conf-gtksourceview3" ) )
   ( "alt-ergo-free" | "alt-ergo" )
   "conf-graphviz" { post }
-  "yojson"
-  "why3" { >= "1.3.3" }
   "conf-time" { with-test }
+  "ocaml" { >= "4.08.1" }
+  "ocamlfind" # needed beyond build stage, used by -load-module
+  "ocamlgraph" { >= "1.8.8" }
+  "why3" { >= "1.3.3" & < "1.4~" }
+  "yojson"
+  "zarith"
 ]
 
 depopts: [
   # cannot use {build}: Frama-C must be recompiled when Coq and libraries changes.
   # Coq: because .vo would would not be loadable by another version of Coq
   # libraries: because we use dynamic linking
+  "apron"
   "coq"
   "mlgmpidl"
-  "apron"
-  "zmq"
   "ppx_deriving"
   "ppx_deriving_yojson"
+  "zmq"
 ]
 
 messages: [
@@ -141,5 +142,5 @@ messages: [
 ]
 
 post-messages: [
-  "Why3 provers setup: rm -r ~/.why3.conf ; why3 config --detect"
+  "Why3 provers setup: rm -f ~/.why3.conf ; why3 config --detect"
 ]