diff --git a/opam b/opam
index bb2473f2092edb0c460ed9d0a2d17e9713526f43..3023744e7dbb86dd1ebdeced08e8a9b304fec14b 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2020-05-24.1.76bec8b7") | (= "dev") }
+  "coq-iris" { (= "dev.2020-05-26.0.e3f87a95") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 1d970dd5e6ae314dc098cd910487fbb353ed8c5b..d136a7e04a956ef93c22e737050bcbb6ae1e1bad 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -250,15 +250,15 @@ Section proof.
       rel_load_l. repeat rel_pure_l.
       rel_store_l_atomic.
       iInv sizeN as (m' ls') "(Ha & >Hs1' & >Hs2' & >Htbl1' & >Htbl2' & #Hls)" "Hcl".
-      iDestruct (gen_heap.mapsto_agree with "Hs1 Hs1'") as %Hm'.
+      iDestruct (mapsto_agree with "Hs1 Hs1'") as %Hm'.
       simplify_eq/=.
       iCombine "Hs1 Hs1'" as "Hs1".
-      iDestruct (gen_heap.mapsto_agree with "Htbl1 Htbl1'") as %->.
+      iDestruct (mapsto_agree with "Htbl1 Htbl1'") as %->.
       iModIntro. iExists _. iFrame. iNext. iIntros "[Hs1 Hs1']".
       repeat rel_pure_l.
       rel_apply_r (refines_acquire_r with "Hl2").
       iIntros "Hl2". repeat rel_pure_r.
-      iDestruct (mapsto_half_combine with "Hs2 Hs2'") as "[% Hs2]"; simplify_eq.
+      iDestruct (mapstoS_half_combine with "Hs2 Hs2'") as "[% Hs2]"; simplify_eq.
       rel_load_r. repeat rel_pure_r.
       rel_store_r. repeat rel_pure_r.
       (* Before we close the lock, we need to gather some evidence *)
@@ -277,7 +277,7 @@ Section proof.
       iCombine "Htbl1 Htbl1'" as "Htbl1".
       iModIntro. iExists _. iFrame. iNext. iIntros "[Htbl1 Htbl1']".
       repeat rel_pure_l. repeat rel_pure_r. rel_load_r.
-      iDestruct (mapsto_half_combine with "Htbl2 Htbl2'") as "[% Htbl2]"; simplify_eq.
+      iDestruct (mapstoS_half_combine with "Htbl2 Htbl2'") as "[% Htbl2]"; simplify_eq.
       repeat rel_pure_r. rel_store_r. repeat rel_pure_r.
       rel_apply_r (refines_release_r with "Hl2").
       iIntros "Hl2". repeat rel_pure_r.
@@ -329,15 +329,15 @@ Section proof.
       rel_load_l. repeat rel_pure_l.
       rel_store_l_atomic.
       iInv sizeN as (m' ls') "(Ha & >Hs1' & >Hs2' & >Htbl1' & >Htbl2' & #Hls)" "Hcl".
-      iDestruct (gen_heap.mapsto_agree with "Hs1 Hs1'") as %Hm'.
+      iDestruct (mapsto_agree with "Hs1 Hs1'") as %Hm'.
       simplify_eq/=.
       iCombine "Hs1 Hs1'" as "Hs1".
-      iDestruct (gen_heap.mapsto_agree with "Htbl1 Htbl1'") as %->.
+      iDestruct (mapsto_agree with "Htbl1 Htbl1'") as %->.
       iModIntro. iExists _. iFrame. iNext. iIntros "[Hs1 Hs1']".
       repeat rel_pure_l.
       rel_apply_r (refines_acquire_r with "Hl2").
       iIntros "Hl2". repeat rel_pure_r.
-      iDestruct (mapsto_half_combine with "Hs2 Hs2'") as "[% Hs2]"; simplify_eq.
+      iDestruct (mapstoS_half_combine with "Hs2 Hs2'") as "[% Hs2]"; simplify_eq.
       rel_load_r. repeat rel_pure_r.
       rel_store_r. repeat rel_pure_r.
       (* Before we close the lock, we need to gather some evidence *)
@@ -352,11 +352,11 @@ Section proof.
       rel_store_l_atomic.
       iClear "Hls".
       iInv sizeN as (m ls) "(Ha & >Hs1 & >Hs2 & >Htbl1 & >Htbl2 & #Hls)" "Hcl".
-      iDestruct (gen_heap.mapsto_agree with "Htbl1 Htbl1'") as %->.
+      iDestruct (mapsto_agree with "Htbl1 Htbl1'") as %->.
       iCombine "Htbl1 Htbl1'" as "Htbl1".
       iModIntro. iExists _. iFrame. iNext. iIntros "[Htbl1 Htbl1']".
       repeat rel_pure_l. repeat rel_pure_r. rel_load_r.
-      iDestruct (mapsto_half_combine with "Htbl2 Htbl2'") as "[% Htbl2]"; simplify_eq.
+      iDestruct (mapstoS_half_combine with "Htbl2 Htbl2'") as "[% Htbl2]"; simplify_eq.
       repeat rel_pure_r. rel_store_r. repeat rel_pure_r.
       rel_apply_r (refines_release_r with "Hl2").
       iIntros "Hl2". repeat rel_pure_r.
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 7c29e430b5791a5ee20503b7d4361572b291f187..d986b6337d0c3162847e4ff1c4d714383288a5e6 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -222,7 +222,7 @@ Section proofs.
         rel_load_l. rel_pure_l. rel_pure_r.
         rel_store_l_atomic.
         iInv i3n as (n') "(>Hx & Hx' & >Hbb)" "Hcl".
-        iDestruct (gen_heap.mapsto_agree with "Hx Hx1") as %->.
+        iDestruct (mapsto_agree with "Hx Hx1") as %->.
         iCombine "Hx Hx1" as "Hx".
         iModIntro. iExists _; iFrame. iNext.
         iIntros "Hx".
@@ -232,7 +232,7 @@ Section proofs.
         iDestruct "Hx'" as "[Hx' Hx'1]".
         iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | Hbb]".
         { iCombine "Hx Hx1" as "Hx".
-          iDestruct (gen_heap.mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
+          iDestruct (mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
           compute in Hfoo. eauto. }
         iMod ("Hcl" with "[Hx Hx' Hbb]") as "_".
         { iNext. iExists (S n).
@@ -241,10 +241,10 @@ Section proofs.
         repeat rel_pure_l. repeat rel_pure_r.
         rel_store_l_atomic. clear n'.
         iInv i3n as (n') "(>Hx & Hx' & >Hbb)" "Hcl".
-        iDestruct (gen_heap.mapsto_agree with "Hx Hx1") as %->.
+        iDestruct (mapsto_agree with "Hx Hx1") as %->.
         iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | (Hb & Hb')]".
         { iCombine "Hx Hx1" as "Hx".
-          iDestruct (gen_heap.mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
+          iDestruct (mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
           compute in Hfoo. eauto. }
         iModIntro; iExists _; iFrame; iNext. iIntros "Hb".
         rel_store_r.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index ae804f7849c6240c708e5443c103741265c23302..cfc792d2d64fff41b119715d8924ba8b2fb86864 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -186,7 +186,7 @@ Section semtypes_properties.
     iInv (relocN.@"ref".@(l1', l)) as (? ?) "(? & >Hl & ?)" "Hcl".
     iInv (relocN.@"ref".@(l2', l)) as (? ?) "(? & >Hl' & ?)" "Hcl'".
     simpl. iExFalso.
-    iDestruct (mapsto_valid_2 with "Hl Hl'") as %Hfoo.
+    iDestruct (mapstoS_valid_2 with "Hl Hl'") as %Hfoo.
     compute in Hfoo. eauto.
   Qed.
 
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index ce4370c1abfc9abe8baa505ea46bab9d6aa651ae..d9e17548faeba7994b743f1f556348fad29eed83 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -2,7 +2,8 @@
 (** A resource algebra for the specification programs. *)
 From iris.algebra Require Import auth excl gmap agree list frac.
 From iris.bi Require Export fractional.
-From iris.base_logic Require Export gen_heap invariants.
+From iris.base_logic Require Import gen_heap.
+From iris.base_logic Require Export invariants.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang lifting.
 Import uPred.
@@ -12,7 +13,7 @@ Definition specN := relocN .@ "spec".
 
 (** The CMRA for the heap of the specification. *)
 Definition tpoolUR : ucmraT := gmapUR nat (exclR exprO).
-Definition cfgUR := prodUR tpoolUR (gen_heapUR loc val).
+Definition cfgUR := prodUR tpoolUR (gen_heapUR loc (option val)).
 
 (** The CMRA for the thread pool. *)
 Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }.
@@ -27,7 +28,7 @@ Section definitionsS.
   Context `{cfgSG Σ, invG Σ}.
 
   Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
-    own cfg_name (◯ (∅, {[ l := (q, to_agree v) ]})).
+    own cfg_name (◯ (∅, {[ l := (q, to_agree (Some v)) ]})).
   Definition heapS_mapsto_aux : { x | x = @heapS_mapsto_def }. by eexists. Qed.
   Definition heapS_mapsto := proj1_sig heapS_mapsto_aux.
   Definition heapS_mapsto_eq :
@@ -40,7 +41,7 @@ Section definitionsS.
   Definition tpool_mapsto_eq :
     @tpool_mapsto = @tpool_mapsto_def := proj2_sig tpool_mapsto_aux.
 
-  Definition mkstate (σ : gmap loc val) (κs : gset proph_id) :=
+  Definition mkstate (σ : gmap loc (option val)) (κs : gset proph_id) :=
     {| heap := σ; used_proph_id := κs |}.
   Definition spec_inv ρ : iProp Σ :=
     (∃ tp σ, own cfg_name (● (to_tpool tp, to_gen_heap (heap σ)))
@@ -124,16 +125,16 @@ End conversions.
 Section mapsto.
   Context `{cfgSG Σ}.
 
-  Global Instance mapsto_fractional l v : Fractional (λ q, l ↦ₛ{q} v)%I.
+  Global Instance mapstoS_fractional l v : Fractional (λ q, l ↦ₛ{q} v)%I.
   Proof.
     intros p q. rewrite heapS_mapsto_eq -own_op -auth_frag_op.
     by rewrite -pair_op singleton_op -pair_op agree_idemp right_id.
   Qed.
-  Global Instance mapsto_as_fractional l q v :
+  Global Instance mapstoS_as_fractional l q v :
     AsFractional (l ↦ₛ{q} v) (λ q, l ↦ₛ{q} v)%I q.
   Proof. split. done. apply _. Qed.
 
-  Lemma mapsto_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ⌜v1 = v2⌝.
+  Lemma mapstoS_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
     apply bi.wand_intro_r.
     rewrite heapS_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
@@ -141,10 +142,10 @@ Section mapsto.
     rewrite -pair_op singleton_op right_id -pair_op.
     move=> [_ Hv]. move:Hv => /=.
     rewrite singleton_valid.
-    by intros [_ ?%agree_op_invL'].
+    by move=> [_] /agree_op_invL' [->].
   Qed.
 
-  Lemma mapsto_valid l q v : l ↦ₛ{q} v -∗ ✓ q.
+  Lemma mapstoS_valid l q v : l ↦ₛ{q} v -∗ ✓ q.
   Proof.
     rewrite heapS_mapsto_eq /heapS_mapsto_def own_valid !uPred.discrete_valid.
     apply pure_mono=> /auth_frag_valid /= [_ Hfoo].
@@ -152,17 +153,17 @@ Section mapsto.
     by intros [? _].
   Qed.
 
-  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ✓ (q1 + q2)%Qp.
+  Lemma mapstoS_valid_2 l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ✓ (q1 + q2)%Qp.
   Proof.
-    iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %->.
-    iApply (mapsto_valid l _ v2). by iFrame.
+    iIntros "H1 H2". iDestruct (mapstoS_agree with "H1 H2") as %->.
+    iApply (mapstoS_valid l _ v2). by iFrame.
   Qed.
 
-  Lemma mapsto_half_combine l v1 v2 :
+  Lemma mapstoS_half_combine l v1 v2 :
     l ↦ₛ{1/2} v1 -∗ l ↦ₛ{1/2} v2 -∗ ⌜v1 = v2⌝ ∗ l ↦ₛ v1.
   Proof.
     iIntros "Hl1 Hl2".
-    iDestruct (mapsto_agree with "Hl1 Hl2") as %?. simplify_eq.
+    iDestruct (mapstoS_agree with "Hl1 Hl2") as %?. simplify_eq.
     iSplit; eauto.
     iApply (fractional_half_2 with "Hl1 Hl2").
   Qed.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 3f0079a6a137bf06b08f6bec244ff4d88fe4f9c1..f22546c9b4cb126abfb0a2ffda1057021ded4688 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -1,10 +1,12 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Rules for updating the specification program. *)
 From iris.algebra Require Import auth excl frac agree gmap list.
+From iris.base_logic.lib Require Import gen_heap.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Export lang notation tactics.
 From reloc.logic Require Export spec_ra.
 Import uPred.
+
 Section rules.
   Context `{relocG Σ}.
   Implicit Types P Q : iProp Σ.
@@ -157,11 +159,11 @@ Section rules.
         singleton_local_update, (exclusive_local_update _ (Excl (fill K (#l)%E))). }
     iMod (own_update with "Hown") as "[Hown Hl]".
     { eapply auth_update_alloc, prod_local_update_2,
-        (alloc_singleton_local_update _ l (1%Qp,to_agree v)); last done.
+        (alloc_singleton_local_update _ l (1%Qp,to_agree (Some v : leibnizO _))); last done.
       by apply lookup_to_gen_heap_None. }
     rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
     iExists l. iFrame "Hj Hl". iApply "Hclose". iNext.
-    iExists (<[j:=fill K (# l)]> tp), (state_upd_heap <[l:=v]> σ).
+    iExists (<[j:=fill K (# l)]> tp), (state_upd_heap <[l:=Some v]> σ).
     rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto.
     rewrite -state_init_heap_singleton. eapply AllocNS; first by lia.
@@ -181,7 +183,8 @@ Section rules.
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
     iDestruct (own_valid_2 with "Hown Hl")
-      as %[[? ?%gen_heap_singleton_included]%prod_included ?]%auth_both_valid.     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
+      as %[[? ?%gen_heap_singleton_included]%prod_included ?]%auth_both_valid.
+    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (of_val v)))). }
     iFrame "Hj Hl". iApply "Hclose". iNext.
@@ -209,11 +212,14 @@ Section rules.
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K #()))). }
     iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
-    { eapply auth_update, prod_local_update_2, singleton_local_update,
-        (exclusive_local_update _ (1%Qp, to_agree v)); last done.
-      by rewrite /to_gen_heap lookup_fmap Hl. }
+    { eapply auth_update, prod_local_update_2.
+      apply: singleton_local_update.
+      { by rewrite /to_gen_heap lookup_fmap Hl. }
+      apply: (exclusive_local_update _
+        (1%Qp, to_agree (Some v : leibnizO (option val)))).
+      apply: pair_exclusive_l. done. }
     iFrame "Hj Hl". iApply "Hclose". iNext.
-    iExists (<[j:=fill K #()]> tp), (state_upd_heap <[l:=v]> σ).
+    iExists (<[j:=fill K #()]> tp), (state_upd_heap <[l:=Some v]> σ).
     rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
   Qed.
@@ -267,11 +273,14 @@ Section rules.
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (_, #true)%V))). }
     iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
-    { eapply auth_update, prod_local_update_2, singleton_local_update,
-        (exclusive_local_update _ (1%Qp, to_agree v2)); last done.
-      by rewrite /to_gen_heap lookup_fmap Hl. }
+    { eapply auth_update, prod_local_update_2.
+      apply: singleton_local_update.
+      { by rewrite /to_gen_heap lookup_fmap Hl. }
+      apply: (exclusive_local_update _
+        (1%Qp, to_agree (Some v2 : leibnizO (option val)))).
+      apply: pair_exclusive_l. done. }
     iFrame "Hj Hl". iApply "Hclose". iNext.
-    iExists (<[j:=fill K (_, #true)%V]> tp), (state_upd_heap <[l:=v2]> σ).
+    iExists (<[j:=fill K (_, #true)%V]> tp), (state_upd_heap <[l:=Some v2]> σ).
     rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
     rewrite bool_decide_true //.
@@ -295,11 +304,14 @@ Section rules.
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (# i1)))). }
     iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
-    { eapply auth_update, prod_local_update_2, singleton_local_update,
-        (exclusive_local_update _ (1%Qp, to_agree #(i1+i2))); last done.
-      by rewrite /to_gen_heap lookup_fmap Hl. }
+    { eapply auth_update, prod_local_update_2.
+      apply: singleton_local_update.
+      { by rewrite /to_gen_heap lookup_fmap Hl. }
+      apply: (exclusive_local_update _
+        (1%Qp, to_agree (Some #(i1+i2) : leibnizO (option val)))).
+      apply: pair_exclusive_l. done. }
     iFrame "Hj Hl". iApply "Hclose". iNext.
-    iExists (<[j:=fill K (# i1)]> tp), (state_upd_heap <[l:=#(i1+i2)]> σ).
+    iExists (<[j:=fill K (# i1)]> tp), (state_upd_heap <[l:=Some #(i1+i2)]> σ).
     rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. simpl. econstructor; eauto.
   Qed.
diff --git a/theories/prelude/ctx_subst.v b/theories/prelude/ctx_subst.v
index a8f2b6794b99adf10c105a65025b11eee1942f84..1668ce07458af5b4457e51acb712afe480421650 100644
--- a/theories/prelude/ctx_subst.v
+++ b/theories/prelude/ctx_subst.v
@@ -21,6 +21,7 @@ Fixpoint subst_map_ctx_item (es : stringmap val) (K : ectx_item)
   | CaseCtx e1 e2 => CaseCtx (subst_map es e1) (subst_map es e2)
   | AllocNLCtx v2 => AllocNLCtx v2
   | AllocNRCtx e1 => AllocNRCtx (subst_map es e1)
+  | FreeCtx => FreeCtx
   | LoadCtx => LoadCtx
   | StoreLCtx v2 => StoreLCtx v2
   | StoreRCtx e1 => StoreRCtx (subst_map es e1)