diff --git a/opam b/opam
index 08e2cbf0932a974a1294f0f75101798785423aed..421efdf5e1da0f99249b156aefb16bf9abc22663 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.2019-05-24.0.c9984c7f") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-01.2.88c7fc6d") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index bc9b1ff7ac534ec1f8bc559655a6a219e5dc968a..78b0437a69de4265b8ca66e9a7926ac6266a13ac 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -159,7 +159,9 @@ Section rules.
     iExists l. iFrame "Hj Hl". iApply "Hclose". iNext.
     iExists (<[j:=fill K (# l)]> tp), (state_upd_heap <[l:=v]> σ).
     rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
-    eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
+    eapply rtc_r, step_insert_no_fork; eauto.
+    rewrite -state_init_heap_singleton. eapply AllocNS; first by lia.
+    intros. assert (i = 0) as -> by lia. by rewrite loc_add_0.
   Qed.
 
   Lemma step_load E ρ j K l q v:
diff --git a/theories/prelude/ctx_subst.v b/theories/prelude/ctx_subst.v
index 81ee397418dec72168fcf82b8fe80808a98a56b0..8b633b66defe8cf1503973dbd2d0916b4a69e70e 100644
--- a/theories/prelude/ctx_subst.v
+++ b/theories/prelude/ctx_subst.v
@@ -19,7 +19,8 @@ Fixpoint subst_map_ctx_item (es : stringmap val) (K : ectx_item)
   | InjLCtx => InjLCtx
   | InjRCtx => InjRCtx
   | CaseCtx e1 e2 => CaseCtx (subst_map es e1) (subst_map es e2)
-  | AllocCtx => AllocCtx
+  | AllocNLCtx v2 => AllocNLCtx v2
+  | AllocNRCtx e1 => AllocNRCtx (subst_map es e1)
   | LoadCtx => LoadCtx
   | StoreLCtx v2 => StoreLCtx v2
   | StoreRCtx e1 => StoreRCtx (subst_map es e1)
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 6f97fbb30de37daf01333bb18b36562d06a63cf1..f1cdffa1eda90843a1428aa6a57e234d4a5c2900 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -157,7 +157,7 @@ where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
 
 Lemma binop_nat_typed_safe (op : bin_op) (n1 n2 : Z) Ï„ :
   binop_nat_res_type op = Some τ → is_Some (bin_op_eval op #n1 #n2).
-Proof. destruct op; simpl; eauto. Qed.
+Proof. destruct op; simpl; eauto. discriminate. Qed.
 
 Lemma binop_bool_typed_safe (op : bin_op) (b1 b2 : bool) Ï„ :
   binop_bool_res_type op = Some τ → is_Some (bin_op_eval op #b1 #b2).