diff --git a/src/plugins/wp/Auto.mli b/src/plugins/wp/Auto.mli
index 6b5234198a8d8392f8666e32b77c33cfaf0047fa..669b50df4c8a7b94c115fc5cb6c7eb4cbad5d972 100644
--- a/src/plugins/wp/Auto.mli
+++ b/src/plugins/wp/Auto.mli
@@ -35,7 +35,7 @@ val contrapose : ?priority:float -> selection -> strategy
 val compound : ?priority:float -> selection -> strategy
 val cut : ?priority:float -> ?modus:bool -> selection -> strategy
 val filter : ?priority:float -> ?anti:bool -> unit -> strategy
-val havoc : ?priority:float -> havoc:selection -> strategy
+val havoc : ?priority:float -> selection -> strategy
 val separated : ?priority:float -> selection -> strategy
 val instance : ?priority:float -> selection -> selection list -> strategy
 val lemma : ?priority:float -> ?at:selection -> string -> selection list -> strategy
diff --git a/src/plugins/wp/TacHavoc.ml b/src/plugins/wp/TacHavoc.ml
index f363cf4ecc86d90c71fd51c3eb131165fef1c002..294c706e6b6342ef1337ccebff69b54da3620fc3 100644
--- a/src/plugins/wp/TacHavoc.ml
+++ b/src/plugins/wp/TacHavoc.ml
@@ -196,7 +196,7 @@ class validity =
 module Havoc =
 struct
   let tactical = Tactical.export (new havoc)
-  let strategy ?(priority=1.0) ~havoc =
+  let strategy ?(priority=1.0) havoc =
     Strategy.{
       priority ;
       tactical ;
diff --git a/src/plugins/wp/TacHavoc.mli b/src/plugins/wp/TacHavoc.mli
index 0942b43ac08e40faf0cfa83bc9f542affb988a3c..de44ed3601eaeba6c3757cf35397db333d725339 100644
--- a/src/plugins/wp/TacHavoc.mli
+++ b/src/plugins/wp/TacHavoc.mli
@@ -29,7 +29,7 @@ module Havoc :
 sig
   val tactical : tactical
   val strategy :
-    ?priority:float -> havoc:selection -> strategy
+    ?priority:float -> selection -> strategy
 end
 
 module Separated :