diff --git a/opam b/opam
index 04fbbb3d94a06e385fe5fd26eec7fb2507dfccc3..5bc8ccbd64ce747b675b4a9898c352241696a41f 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2019-06-09.3.31bf88ff") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-10.2.47f304f6") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/logrel/F_mu_ref/rules.v b/theories/logrel/F_mu_ref/rules.v
index 160241bbf241b00df1f4c55b069d3428b13bd380..f2418db76000ea68044890c394d883b416158855 100644
--- a/theories/logrel/F_mu_ref/rules.v
+++ b/theories/logrel/F_mu_ref/rules.v
@@ -65,7 +65,7 @@ Section lang_rules.
     iApply wp_lift_atomic_head_step_no_fork; auto.
     iIntros (σ1 ???) "Hσ !>"; iSplit; first by auto.
     iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
-    iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
+    iMod (@gen_heap_alloc with "Hσ") as "(Hσ & Hl & _)"; first done.
     iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
   Qed.
 
diff --git a/theories/logrel/F_mu_ref/soundness.v b/theories/logrel/F_mu_ref/soundness.v
index bf92b9e252ceee1932215da797164c93a885490b..f75f2312c47970d3f6ee8c85c281db4e94f2ab37 100644
--- a/theories/logrel/F_mu_ref/soundness.v
+++ b/theories/logrel/F_mu_ref/soundness.v
@@ -16,10 +16,9 @@ Proof.
   intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
   eapply (wp_adequacy Σ _); eauto.
   iIntros (Hinv ?).
-  iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
-  { by apply auth_auth_valid, to_gen_heap_valid. }
-  iModIntro. iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
-  set (HeapΣ := (HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
+  iMod (gen_heap_init σ) as (Hheap) "Hh".
+  iModIntro. iExists (λ σ _, gen_heap_ctx σ); iFrame.
+  set (HeapΣ := (HeapG Σ Hinv Hheap)).
   iApply (wp_wand with "[]").
   - replace e with e.[env_subst[]] by by asimpl.
     iApply (Hlog HeapΣ [] []). iApply (@interp_env_nil _ HeapΣ).
diff --git a/theories/logrel/F_mu_ref/soundness_binary.v b/theories/logrel/F_mu_ref/soundness_binary.v
index 5fabf6ec0d29bcd43bc1fdd5df14396938577eac..00bbf0c8f2e08efacdf50e39c937615866a9593c 100644
--- a/theories/logrel/F_mu_ref/soundness_binary.v
+++ b/theories/logrel/F_mu_ref/soundness_binary.v
@@ -15,8 +15,7 @@ Proof.
   { destruct 1; naive_solver. }
   eapply (wp_adequacy Σ); first by apply _.
   iIntros (Hinv ?).
-  iMod (own_alloc (● to_gen_heap ∅)) as (γ) "Hh".
-  { by apply auth_auth_valid, to_gen_heap_valid. }
+  iMod (gen_heap_init (∅: state)) as (Hheap) "Hh".
   iMod (own_alloc (● (Excl' e', ∅)
     ⋅ ◯ ((Excl' e', ∅) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
   { apply auth_both_valid. split=>//. }
@@ -25,8 +24,8 @@ Proof.
   { iNext. iExists e', ∅. iSplit; eauto.
     rewrite /to_gen_heap fin_maps.map_fmap_empty.
     iFrame. }
-  set (HeapΣ := HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ)).
-  iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
+  set (HeapΣ := HeapG Σ Hinv Hheap).
+  iExists (λ σ _, gen_heap_ctx σ); iFrame.
   iApply wp_fupd. iApply (wp_wand with "[-]").
   - iPoseProof (Hlog _ _ with "[$Hcfg]") as "Hrel".
     { iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
diff --git a/theories/logrel/F_mu_ref_conc/rules.v b/theories/logrel/F_mu_ref_conc/rules.v
index 7ad1345633582b475d7e1f62cab0828154bd2200..ef74a3976dbbc9dad46bc75b0f32ff1e2bdff001 100644
--- a/theories/logrel/F_mu_ref_conc/rules.v
+++ b/theories/logrel/F_mu_ref_conc/rules.v
@@ -60,7 +60,7 @@ Section lang_rules.
     iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
     iIntros (σ1 ???) "Hσ !>"; iSplit; first by auto.
     iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
-    iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
+    iMod (@gen_heap_alloc with "Hσ") as "(Hσ & Hl & _)"; first done.
     iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
   Qed.
 
diff --git a/theories/logrel/F_mu_ref_conc/soundness_binary.v b/theories/logrel/F_mu_ref_conc/soundness_binary.v
index 2ce4327f2dfb635bf06d868747d2b73a026ee3c3..bf10c67126d424921d277bd7b701e2a9ca4f731a 100644
--- a/theories/logrel/F_mu_ref_conc/soundness_binary.v
+++ b/theories/logrel/F_mu_ref_conc/soundness_binary.v
@@ -14,16 +14,15 @@ Proof.
   cut (adequate NotStuck e ∅ (λ _ _, ∃ thp' h v, rtc erased_step ([e'], ∅) (of_val v :: thp', h))).
   { destruct 1; naive_solver. }
   eapply (wp_adequacy Σ _); iIntros (Hinv ?).
-  iMod (own_alloc (● to_gen_heap ∅)) as (γ) "Hh".
-  { by apply auth_auth_valid, to_gen_heap_valid. }
+  iMod (gen_heap_init (∅: state)) as (Hheap) "Hh".
   iMod (own_alloc (● (to_tpool [e'], ∅)
     ⋅ ◯ ((to_tpool [e'] : tpoolUR, ∅) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
   { apply auth_both_valid. split=>//. split=>//. apply to_tpool_valid. }
   set (Hcfg := CFGSG _ _ γc).
   iMod (inv_alloc specN _ (spec_inv ([e'], ∅)) with "[Hcfg1]") as "#Hcfg".
   { iNext. iExists [e'], ∅. rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
-  set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
-  iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
+  set (HeapΣ := (HeapIG Σ Hinv Hheap)).
+  iExists (λ σ _, gen_heap_ctx σ); iFrame.
   iApply wp_fupd. iApply wp_wand_r.
   iSplitL.
   iPoseProof ((Hlog _ _ [] []) with "[]") as "Hrel".
diff --git a/theories/logrel/F_mu_ref_conc/soundness_unary.v b/theories/logrel/F_mu_ref_conc/soundness_unary.v
index 293c606c8a99425e9a529d032fe2005483c73640..7a1213f2bcb096c6e509add2c727acb6cb0e3db0 100644
--- a/theories/logrel/F_mu_ref_conc/soundness_unary.v
+++ b/theories/logrel/F_mu_ref_conc/soundness_unary.v
@@ -15,10 +15,9 @@ Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' :
 Proof.
   intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
   eapply (wp_adequacy Σ _). iIntros (Hinv ?).
-  iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
-  { by apply auth_auth_valid, to_gen_heap_valid. }
-  iModIntro. iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
-  set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
+  iMod (gen_heap_init σ) as (Hheap) "Hh".
+  iModIntro. iExists (λ σ _, gen_heap_ctx σ); iFrame.
+  set (HeapΣ := (HeapIG Σ Hinv Hheap)).
   iApply (wp_wand with "[]").
   - replace e with e.[env_subst[]] by by asimpl.
     iApply (Hlog HeapΣ [] []). iApply (@interp_env_nil _ HeapΣ).