diff --git a/opam b/opam
index caf743533132d922d0d5f5d180f98b396713bc0b..0d644dc9035c66a72b92f5b5e4e2fb9e006c5d8d 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 da1d71e90b442861f50d6087cdf94253f4f5378d..35f9503727d13f1854ee4afd307b83cead02d191 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 987c09e9bceb9fd7724d8a1d4e133548759b3f54..bb28917bf5a4434f088919f30cb23142ec3af8bd 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.