diff --git a/opam b/opam
index 52a3406c05020560ff529d40488fab56c7c6423d..fc9bcb0a5151c168026283e7cee2e6244786c9f8 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-04-20.0.7a260d80") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-05-27.2.59e3a162") | (= "dev") }
 ]
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index f7008ba8819ed2efce5933544b830e15e1a6fb36..2c91fda189283b5687a90cab2ce281e5211f1d47 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -1287,9 +1287,9 @@ Section proto.
   Qed.
 
   Global Instance iProto_le_from_modal a v p1 p2 :
-    FromModal (modality_instances.modality_laterN 1) (p1 ⊑ p2)
+    FromModal True (modality_instances.modality_laterN 1) (p1 ⊑ p2)
               ((<a> MSG v; p1) ⊑ (<a> MSG v; p2)) (p1 ⊑ p2).
-  Proof. apply iProto_le_base. Qed.
+  Proof. intros _. apply iProto_le_base. Qed.
 
 End proto.
 
diff --git a/theories/examples/swap_mapper.v b/theories/examples/swap_mapper.v
index cbb3df7c485708a16708ebafeada792c528f03a5..22adfcd013995d8ef72377c83b0e540ab1aa90c6 100644
--- a/theories/examples/swap_mapper.v
+++ b/theories/examples/swap_mapper.v
@@ -71,9 +71,9 @@ Section with_Σ.
   Qed.
 
   Global Instance send_once_from_modal p1 p2 :
-    FromModal (modality_instances.modality_laterN 1) (∀ x, p1 x ⊑ p2 x)
+    FromModal True (modality_instances.modality_laterN 1) (∀ x, p1 x ⊑ p2 x)
               ((send_once p1) ⊑ (send_once p2)) (∀ x, p1 x ⊑ p2 x).
-  Proof. apply send_once_mono. Qed.
+  Proof. intros _. apply send_once_mono. Qed.
 
   Lemma recv_once_mono prot1 prot2 x :
     ▷ (prot1 ⊑ prot2) -∗ recv_once prot1 x ⊑ recv_once prot2 x.
@@ -84,18 +84,18 @@ Section with_Σ.
   Qed.
 
   Global Instance recv_once_from_modal p1 p2 x :
-    FromModal (modality_instances.modality_laterN 1) (p1 ⊑ p2)
+    FromModal True (modality_instances.modality_laterN 1) (p1 ⊑ p2)
               ((recv_once p1 x) ⊑ (recv_once p2 x)) (p1 ⊑ p2).
-  Proof. apply recv_once_mono. Qed.
+  Proof. intros _. apply recv_once_mono. Qed.
 
   Lemma map_once_mono prot1 prot2 :
     ▷ (prot1 ⊑ prot2) -∗ map_once prot1 ⊑ map_once prot2.
   Proof. iIntros "Hsub". iModIntro. iIntros (x). iModIntro. eauto. Qed.
 
   Global Instance map_once_from_modal p1 p2 :
-    FromModal (modality_instances.modality_laterN 1) (p1 ⊑ p2)
+    FromModal True (modality_instances.modality_laterN 1) (p1 ⊑ p2)
               ((map_once p1) ⊑ (map_once p2)) (p1 ⊑ p2).
-  Proof. apply map_once_mono. Qed.
+  Proof. intros _. apply map_once_mono. Qed.
 
   Definition mapper_prot_once :=
     (map_once mapper_prot)%proto.
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 081681e4596b976f0f2f18b6a1210e5d52140007..d87b685decafe52ac817bcfe70bd8c22aaad9720 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -450,17 +450,17 @@ Section subtyping_rules.
   Qed.
 
   Global Instance lty_le_from_modal_send A (S1 S2 : lsty Σ) :
-    FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
+    FromModal True (modality_instances.modality_laterN 1) (S1 <: S2)
               ((<!!> TY A; S1) <: (<!!> TY A; S2)) (S1 <: S2) | 0.
   Proof.
-    rewrite /FromModal. iIntros "H". iApply lty_le_send. iApply lty_le_refl. done.
+    rewrite /FromModal. iIntros (_) "H". iApply lty_le_send. iApply lty_le_refl. done.
   Qed.
 
   Global Instance lty_le_from_modal_recv A (S1 S2 : lsty Σ) :
-    FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
+    FromModal True (modality_instances.modality_laterN 1) (S1 <: S2)
               ((<??> TY A; S1) <: (<??> TY A; S2)) (S1 <: S2) | 0.
   Proof.
-    rewrite /FromModal. iIntros "H". iApply lty_le_recv. iApply lty_le_refl. done.
+    rewrite /FromModal. iIntros (_) "H". iApply lty_le_recv. iApply lty_le_refl. done.
   Qed.
 
   (** Algebraic laws *)