From a4237b930de25a919a160276531f884b5a0ad504 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 9 Feb 2018 13:51:59 +0100
Subject: [PATCH] fix for Iris bump

---
 opam                           | 2 +-
 theories/lang/lib/new_delete.v | 2 +-
 theories/typing/lib/arc.v      | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/opam b/opam
index caf74353..0d644dc9 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2018-01-21.0") | (= "dev") }
+  "coq-iris" { (= "dev.2018-02-09.0") | (= "dev") }
 ]
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index da1d71e9..35f95037 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -26,7 +26,7 @@ Section specs.
     - wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
       rewrite heap_mapsto_vec_nil. auto.
     - wp_if. wp_alloc l as "H↦" "H†". omega. iApply "HΦ". subst sz.
-      iFrame. auto.
+      iFrame.
   Qed.
 
   Lemma wp_delete E (n:Z) l vl :
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 987c09e9..bb28917b 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -820,7 +820,7 @@ Section arc.
     { destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
       iDestruct "H↦" as (vl) "[? Heq]". iDestruct "Heq" as %<-.
       wp_apply (wp_delete _ _ _ (_::_::vl) with "[-]"); [simpl;lia| |done].
-      rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. auto. }
+      rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. }
     iIntros (?) "_". wp_seq.
     (* Finish up the proof. *)
     iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); r ◁ box (uninit 0) ]
@@ -884,7 +884,7 @@ Section arc.
       { destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
         iDestruct "H↦" as (vl') "[? Heq]". iDestruct "Heq" as %<-.
         wp_apply (wp_delete _ _ _ (_::_::vl') with "[-]"); [simpl; lia| |done].
-        rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. auto. }
+        rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. }
       iIntros (?) "_". wp_seq.
       iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); #r ◁ box (Σ[ ty; arc ty ]) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
-- 
GitLab