From 3845293e483a0a01c971ad113b73867cdd68b95f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 19 Apr 2016 21:35:37 +0200
Subject: [PATCH] proof tuning

---
 heap_lang/lifting.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 1185095ab..3aeaf32f8 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -28,13 +28,13 @@ Lemma wp_alloc_pst E σ e v Φ :
   (▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LocV l)))
   ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
+  iIntros {?}  "[HP HΦ]".
   (* TODO: This works around ssreflect bug #22. *)
-  intros. set (φ (e' : expr []) σ' ef := ∃ l,
+  set (φ (e' : expr []) σ' ef := ∃ l,
     ef = None ∧ e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
-  rewrite -(wp_lift_atomic_head_step (Alloc e) φ σ) // /φ;
-    last (by intros; inv_head_step; eauto 8); last (by simpl; eauto).
-  iIntros  "[HP HΦ]". iFrame "HP". iNext.
-  iIntros {v2 σ2 ef} "[% HP]".
+  iApply (wp_lift_atomic_head_step (Alloc e) φ σ); try (by simpl; eauto);
+    [by intros; subst φ; inv_head_step; eauto 8|].
+  iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]".
   (* FIXME: I should not have to refer to "H0". *)
   destruct H0 as (l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
   iSplit; last done. iApply "HΦ"; by iSplit.
-- 
GitLab