diff --git a/dune-project b/dune-project
index a8bc5091e..4e91002c1 100644
--- a/dune-project
+++ b/dune-project
@@ -21,7 +21,7 @@
   dune-site
   (ocaml-inifiles (>= 1.2))
   (pcre (>= 7))
-  (why3 (and (>= 1.7.0) (< 1.8)))
+  (why3 (and (>= 1.8.0) (< 1.9)))
   yojson
   (zarith (>= 1.10))
 ))
diff --git a/easycrypt.opam b/easycrypt.opam
index 4803cf34a..e8166b256 100644
--- a/easycrypt.opam
+++ b/easycrypt.opam
@@ -9,7 +9,7 @@ depends: [
   "dune-site"
   "ocaml-inifiles" {>= "1.2"}
   "pcre" {>= "7"}
-  "why3" {>= "1.7.0" & < "1.8"}
+  "why3" {>= "1.8.0" & < "1.9"}
   "yojson"
   "zarith" {>= "1.10"}
   "odoc" {with-doc}
diff --git a/src/ecCoq.ml b/src/ecCoq.ml
index 7ef3db66d..43186aa15 100644
--- a/src/ecCoq.ml
+++ b/src/ecCoq.ml
@@ -37,7 +37,7 @@ let run_batch ~(script : string) ~(coqenv : coqenv) (task : WTask.task) =
   let config = Why3.Whyconf.get_main coqenv.config in
   let config_mem = Why3.Whyconf.memlimit config in
   let config_time = Why3.Whyconf.timelimit config in
-  let limit =
+  let limits =
     Why3.Call_provers.{
       limit_time = config_time;
       limit_steps = 0;
@@ -50,7 +50,7 @@ let run_batch ~(script : string) ~(coqenv : coqenv) (task : WTask.task) =
   let call =
     Why3.Driver.prove_task_prepared
       ~old:script ~inplace:true
-      ~command ~limit ~config coqenv.driver task
+      ~command ~limits ~config coqenv.driver task
   in call_prover_task ~coqenv call
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/ecProvers.ml b/src/ecProvers.ml
index ac0955b14..db618f244 100644
--- a/src/ecProvers.ml
+++ b/src/ecProvers.ml
@@ -513,17 +513,17 @@ let run_prover
     let pc =
       let command = pr.Whyconf.command in
 
-      let limit = { Call_provers.empty_limit with
+      let limits = { Call_provers.empty_limits with
         Call_provers.limit_time =
-          let limit = pi.pr_timelimit * pi.pr_cpufactor in
-          if limit <= 0 then 0. else float_of_int limit;
+          let limits = pi.pr_timelimit * pi.pr_cpufactor in
+          if limits <= 0 then 0. else float_of_int limits;
       } in
 
       let rec doit gcdone =
         try
           Driver.prove_task
             ~config:(Config.main ())
-            ~command ~limit dr task
+            ~command ~limits dr task
         with Unix.Unix_error (Unix.ENOMEM, "fork", _) when not gcdone ->
           Gc.compact (); doit true
       in
@@ -618,7 +618,7 @@ let execute_task ?(notify : notify option) (pi : prover_infos) task =
                       let fmt = Format.formatter_of_buffer buf in
                       Format.fprintf fmt "prover %s disproved this goal." prover;
                     Buffer.contents buf)));
-                | (CP.Failure _ | CP.HighFailure) as answer->
+                | (CP.Failure _ | CP.HighFailure _) as answer->
                   notify |> oiter (fun notify -> notify `Warning (lazy (
                     let buf = Buffer.create 0 in
                     let fmt = Format.formatter_of_buffer buf in