bump Iris for array changes

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" }
 ]

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:

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)

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).