From 37713a6a79e34d850d958005cee986ce0a242f4c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 22 Feb 2016 14:53:11 +0100
Subject: [PATCH] move a TODO around
---
heap_lang/tests.v | 2 --
heap_lang/wp_tactics.v | 3 ++-
2 files changed, 2 insertions(+), 3 deletions(-)
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 91021e180..5035a8d3d 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -63,8 +63,6 @@ Section LiftingTests.
Proof.
wp_lam. wp_op=> ?; wp_if.
- wp_op. wp_op.
- (* TODO: Can we use the wp tactic again here? It seems that the tactic fails if there
- are goals being generated. That should not be the case. *)
ewp apply FindPred_spec; last omega.
wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
- by ewp apply FindPred_spec; eauto with omega.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index c461fd748..d1495340c 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -190,6 +190,7 @@ Tactic Notation "wp" ">" tactic(tac) :=
end.
Tactic Notation "wp" tactic(tac) := (wp> tac); [wp_strip_later|..].
-(* In case the precondition does not match *)
+(* In case the precondition does not match.
+ TODO: Have one tactic unifying wp and ewp. *)
Tactic Notation "ewp" tactic(tac) := wp (etrans; [|tac]).
Tactic Notation "ewp" ">" tactic(tac) := wp> (etrans; [|tac]).
--
GitLab