From 06347d84d3f5c6ad6edd71beaec69001ed88e00f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 1 Jun 2019 16:35:43 +0200
Subject: [PATCH] bump Iris for array changes

---
 opam                         | 2 +-
 theories/logic/spec_rules.v  | 4 +++-
 theories/prelude/ctx_subst.v | 3 ++-
 theories/typing/types.v      | 2 +-
 4 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/opam b/opam
index 08e2cbf..421efdf 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 bc9b1ff..78b0437 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 81ee397..8b633b6 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 6f97fbb..f1cdffa 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).
-- 
GitLab