From 876bddaa703d7a6602145dcaa1ccf270776e39eb Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 8 Feb 2021 15:41:31 +0100
Subject: [PATCH] [Wp] remove unerasable-optional-argument warning related to
prove_prop
---
src/plugins/wp/ProverWhy3.ml | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 54e5d9d0cbf..ed48014f562 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1088,7 +1088,7 @@ let prove_goal ~id ~title ~name ?axioms t =
end;
th, decl
-let prove_prop ?axioms ~pid ~prop =
+let prove_prop ?axioms ~pid prop =
let id = WpPropId.get_propid pid in
let title = Pretty_utils.to_string WpPropId.pretty pid in
let name = "WP" in
@@ -1105,13 +1105,13 @@ let task_of_wpo wpo =
let axioms = v.Wpo.VC_Annot.axioms in
let prop = Wpo.GOAL.compute_proof v.Wpo.VC_Annot.goal in
(* Format.printf "Goal: %a@." Lang.F.pp_pred prop; *)
- prove_prop ~pid ~prop ?axioms
+ prove_prop ~pid prop ?axioms
| Wpo.GoalLemma v ->
let lemma = v.Wpo.VC_Lemma.lemma in
let depends = v.Wpo.VC_Lemma.depends in
let prop = Lang.F.p_forall lemma.l_forall lemma.l_lemma in
let axioms = Some(lemma.l_cluster,depends) in
- prove_prop ~pid ~prop ?axioms
+ prove_prop ~pid prop ?axioms
(* -------------------------------------------------------------------------- *)
(* --- Prover Task --- *)
--
GitLab