diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 6e7efb62cfe29b151ceee1175b863c7fcea8571c..ba62ac1d23e4c4376ee171b482ae6f51f3cfc039 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-02-10.0.7b4a04ce") | (= "dev") }
+  "coq-iris" { (= "dev.2021-02-14.0.842fb394") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 11b48b8f1960f6cab9a7bf87a6d9e7016ec6f5b5..a8dca25cf962fce28d96930da8ff3f5aa42ef3dc 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -131,7 +131,7 @@ Section mguard.
     Send ty → Send (mutexguard α ty).
   Proof.
     iIntros (??? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
-    iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_spec.
+    iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_entails.
     repeat match goal with
            | |- (ty_own _ _ _) ≡ (ty_own _ _ _) => by apply send_change_tid'
            | |- _ => f_equiv
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index b5f64b885ae856b7339c5771f4e018667ba23f6d..b4923b117d7ce82f40315b483c2387bd3c1f726e 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -221,7 +221,7 @@ Section rwlock.
     Send ty → Sync ty → Sync (rwlock ty).
   Proof.
     move=>??????/=. do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r.
-    apply bi.equiv_spec. f_equiv.
+    apply bi.equiv_entails. f_equiv.
     by rewrite rwlock_inv_change_tid_own rwlock_inv_change_tid_shr.
   Qed.
 End rwlock.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 55ffb1968f1353f14ec1af33b004e40f80178c46..f3d6ac7841c3ba1b61c0f58d64f4b535fb8adb50 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -128,7 +128,7 @@ Section rwlockreadguard.
     Sync ty → Send (rwlockreadguard α ty).
   Proof.
     iIntros (??? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
-    iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_spec.
+    iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_entails.
     repeat lazymatch goal with
            | |- (ty_shr _ _ _ _) ≡ (ty_shr _ _ _ _) => by apply sync_change_tid'
            | |- (rwlock_inv _ _ _ _ _ _) ≡ _ => by apply rwlock_inv_change_tid_shr
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 651ff4dfb5e0a9a482214245c6d78879e90a54cb..8b5666b389ac56883a527016131f950412d054ed 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -132,7 +132,7 @@ Section rwlockwriteguard.
     Send ty → Send (rwlockwriteguard α ty).
   Proof.
     iIntros (??? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
-    iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_spec.
+    iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_entails.
     repeat lazymatch goal with
            | |- (ty_own _ _ _) ≡ (ty_own _ _ _) => by apply send_change_tid'
            | |- (rwlock_inv _ _ _ _ _ _) ≡ _ => by apply rwlock_inv_change_tid_own