From 19c45f91bd9b513763e2c81f8643b51724edd8cb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Oct 2016 10:57:16 +0200
Subject: [PATCH] fix heap_lang/adequacy

(forgot to add this to the previous commit...)
---
 heap_lang/adequacy.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index a5e84e8d0..654c77748 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -1,28 +1,28 @@
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Export heap.
 From iris.algebra Require Import auth.
-From iris.program_logic Require Import ownership.
+From iris.program_logic Require Import ownership auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
 
 Class heapPreG Σ := HeapPreG {
   heap_preG_iris :> irisPreG heap_lang Σ;
-  heap_preG_heap :> inG Σ (authR heapUR)
+  heap_preG_heap :> authG Σ heapUR
 }.
 
 Definition heapΣ : gFunctors :=
-  #[irisΣ heap_lang; GFunctor (constRF (authR heapUR))].
+  #[irisΣ heap_lang; authΣ heapUR].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
-Proof. intros [? ?%subG_inG]%subG_inv. split; apply _. Qed.
+Proof. intros [? ?]%subG_inv. split; apply _. Qed.
 
 Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
   (∀ `{heapG Σ}, heap_ctx ⊢ WP e {{ v, ■ φ v }}) →
   adequate e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
-  iVs (own_alloc (● to_heap σ)) as (γ) "Hh".
-  { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
+  iVs (auth_alloc to_heap ownP heapN _ σ with "[Hσ]") as (γ) "[Hh _]".
+  { exact: to_heap_valid. }
+  { by iNext. }
   set (Hheap := HeapG _ _ _ γ).
-  iVs (inv_alloc heapN _ heap_inv with "[-]"); [iNext; iExists σ; by iFrame|].
   iApply (Hwp _). by rewrite /heap_ctx.
-Qed.
\ No newline at end of file
+Qed.
-- 
GitLab