diff --git a/opam.pins b/opam.pins
index 90d82d5a4825aa26ed7317a194b7da14330b597b..9d8485267e96fcd0b1e9250252ccb170592478b2 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq e2b843075894275afd52c19c83e4f5f812afdbab
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq adfa07525e071b2a47aed37dac276aa38c10099d
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 1160c6a6973bdd0d018ac384013f8143c4310f22..d62a06cf9076f7271c0cb4426a45868e6c721f10 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -98,36 +98,6 @@ Section type.
     rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
   Qed.
 
-  Lemma na_own_acc F2 F1 tid :
-    F2 ⊆ F1 →
-    na_own tid F1 -∗ na_own tid F2 ∗
-           (na_own tid F2 -∗ na_own tid F1).
-  Proof.
-    intros HF. assert (F1 = F2 ∪ (F1 ∖ F2)) as -> by exact: union_difference_L.
-    rewrite na_own_union; last by set_solver+.
-    iIntros "[$ $]". auto.
-  Qed.
-
-(*  Lemma shr_locsE_get_tok l n F tid :
-    shr_locsE l n ⊆ F →
-    na_own tid F -∗ na_own tid (shr_locsE l n) ∗ 
-         (na_own tid (shr_locsE l n) -∗ na_own tid F).
-  Proof.
-    intros HF.
-    assert (F = shr_locsE l n ∪ (F ∖ shr_locsE l n)) as -> by exact: union_difference_L.
-    rewrite na_own_union; last by set_solver+.
-    iIntros "[$ $]". by iIntros "?".
-  Qed.
-
-  Lemma shr_locsE_get_tokS l n F tid :
-    shr_locsE l (n + 1) ⊆ F →
-    na_own tid F -∗ na_own tid (shr_locsE l n) ∗ 
-         (na_own tid (shr_locsE l n) -∗ na_own tid F).
-  Proof.
-    intros HF. apply shr_locsE_get_tok. rewrite <-HF.
-    apply shr_locsE_subseteq. omega.
-  Qed.
-*)
   (** Copy types *)
   Class Copy (t : type) := {
     copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);