diff --git a/coq-actris.opam b/coq-actris.opam
index 0c6a5cdb8c27e80e9dda5ed5ad68a571edae1c7a..6a4adc2394169adc6146a472da304df39427cdbf 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-05-03.3.85295b18") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-08-03.5.fe2b6d61") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index f23854abe622a94d995bb15e3b3093ee66631fb8..11b1e5279a05cbe67ff0fc61c558897db338ce19 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -482,9 +482,9 @@ Section subtyping_rules.
     (<!!> M) <++> S2 <:>
         <!!.. As> TY (ktele_app A As) ; (ktele_app S As) <++> S2.
   Proof.
-    rewrite /LtyMsgTele. iIntros (->).
+    rewrite /LtyMsgTele. intros ->.
     rewrite /lty_app /lty_message iProto_app_message /=.
-    induction kt as [|k kt IH]; rewrite iMsg_app_exist.
+    induction kt as [|k kt IH]; rewrite /= iMsg_app_exist.
     - iSplit; iIntros (v); iExists v; rewrite iMsg_app_base; eauto.
     - iSplit.
       + iIntros (v). iExists v.
@@ -498,9 +498,9 @@ Section subtyping_rules.
     (<??> M) <++> S2 <:>
         <??.. As> TY (ktele_app A As) ; (ktele_app S As) <++> S2.
   Proof.
-    rewrite /LtyMsgTele. iIntros (->).
+    rewrite /LtyMsgTele. intros ->.
     rewrite /lty_app /lty_message iProto_app_message /=.
-    induction kt as [|k kt IH]; rewrite iMsg_app_exist.
+    induction kt as [|k kt IH]; rewrite /= iMsg_app_exist.
     - iSplit; iIntros (v); iExists v; rewrite iMsg_app_base; eauto.
     - iSplit.
       + iIntros (v). iExists v.
@@ -555,9 +555,9 @@ Section subtyping_rules.
     lty_dual (<!!> M) <:>
         <??.. As> TY (ktele_app A As) ; lty_dual (ktele_app S As).
   Proof.
-    rewrite /LtyMsgTele. iIntros (->).
+    rewrite /LtyMsgTele. intros ->.
     rewrite /lty_dual /lty_message iProto_dual_message /=.
-    induction kt as [|k kt IH]; rewrite iMsg_dual_exist.
+    induction kt as [|k kt IH]; rewrite /= iMsg_dual_exist.
     - iSplit; iIntros (v); iExists v; rewrite iMsg_dual_base; eauto.
     - iSplit.
       + iIntros (v). iExists v.
@@ -571,9 +571,9 @@ Section subtyping_rules.
     lty_dual (<??> M) <:>
       <!!.. As> TY (ktele_app A As) ; lty_dual (ktele_app S As).
   Proof.
-    rewrite /LtyMsgTele. iIntros (->).
+    rewrite /LtyMsgTele. intros ->.
     rewrite /lty_dual /lty_message iProto_dual_message /=.
-    induction kt as [|k kt IH]; rewrite iMsg_dual_exist.
+    induction kt as [|k kt IH]; rewrite /= iMsg_dual_exist.
     - iSplit; iIntros (v); iExists v; rewrite iMsg_dual_base; eauto.
     - iSplit.
       + iIntros (v). iExists v.