From 4c27fb0ab24eba64579df98a32abe4536ce9aeb9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 23 Jun 2016 15:11:45 +0200
Subject: [PATCH] Generalize 7c4416b6 to remove head "value ;;" expressions
after any wp_ tactic.
---
heap_lang/proofmode.v | 2 +-
heap_lang/wp_tactics.v | 8 +++++++-
2 files changed, 8 insertions(+), 2 deletions(-)
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index fa9b31fca..bd01b72a4 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -148,7 +148,7 @@ Tactic Notation "wp_store" :=
|let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
|env_cbv; reflexivity
- |wp_finish; try wp_seq]
+ |wp_finish]
| _ => fail "wp_store: not a 'wp'"
end.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 4f42702a8..aa27dd003 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -22,8 +22,14 @@ Ltac wp_value_head :=
match goal with |- _ ⊢ wp _ _ _ => simpl | _ => fail end)
end.
+Ltac wp_seq_head :=
+ lazymatch goal with
+ | |- _ ⊢ wp ?E (Seq _ _) ?Q => etrans; [|eapply wp_seq; wp_done]; strip_later
+ end.
+
Ltac wp_finish := intros_revert ltac:(
- rewrite /= ?to_of_val; try strip_later; try wp_value_head).
+ rewrite /= ?to_of_val; try strip_later; try wp_value_head);
+ repeat wp_seq_head.
Tactic Notation "wp_value" :=
lazymatch goal with
--
GitLab