From 5b0340e694f3507d3625c0f319fbd0552ca66f6a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Feb 2016 19:59:58 +0100
Subject: [PATCH] notes on wp failing
---
heap_lang/tests.v | 3 ++-
heap_lang/wp_tactics.v | 2 +-
2 files changed, 3 insertions(+), 2 deletions(-)
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index d687c9051..414c82d86 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -63,7 +63,8 @@ Section LiftingTests.
Proof.
wp_lam>; apply later_mono; wp_op=> ?; wp_if.
- wp_op. wp_op.
- (* TODO: Can we use the wp tactic again here? *)
+ (* 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. *)
wp_focus (FindPred _ _). rewrite -FindPred_spec; last by omega.
wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
- rewrite -FindPred_spec; eauto with omega.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index ee6117c9e..6cb031f74 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -141,7 +141,7 @@ Tactic Notation "wp" ">" tactic(tac) :=
match goal with
| |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => wp_bind K; tac)
end.
-Tactic Notation "wp" tactic(tac) := (wp> tac); wp_strip_later.
+Tactic Notation "wp" tactic(tac) := (wp> tac); [wp_strip_later|..].
(* In case the precondition does not match *)
Tactic Notation "ewp" tactic(tac) := wp (etrans; [|tac]).
--
GitLab