From 2f6b8a24691af678f2ec52ee42e6fcfa4b7072a9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Oct 2016 10:59:25 +0200
Subject: [PATCH] shorten heap_lang/adequacy proof

---
 heap_lang/adequacy.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index 654c77748..6da24be01 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -20,9 +20,8 @@ Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
   adequate e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
-  iVs (auth_alloc to_heap ownP heapN _ σ with "[Hσ]") as (γ) "[Hh _]".
+  iVs (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|].
   { exact: to_heap_valid. }
-  { by iNext. }
   set (Hheap := HeapG _ _ _ γ).
   iApply (Hwp _). by rewrite /heap_ctx.
 Qed.
-- 
GitLab