From 78c6d534556b10fd6109a6fb45efd823f387a69c Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 8 Feb 2021 15:43:43 +0100
Subject: [PATCH] [Wp] remove unerasable-optional-argument warning related to
Havoc.strategy
---
src/plugins/wp/Auto.mli | 2 +-
src/plugins/wp/TacHavoc.ml | 2 +-
src/plugins/wp/TacHavoc.mli | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/Auto.mli b/src/plugins/wp/Auto.mli
index 6b5234198a8..669b50df4c8 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 f363cf4ecc8..294c706e6b6 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 0942b43ac08..de44ed3601e 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 :
--
GitLab