diff --git a/opam b/opam
index 760461c035ccca6a5acc54592498835c1bc860fe..aa2413c08e635076bad81bf4b8ba27ee25ac8cd1 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-06-12.0.3cb65333") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-06-18.0.366d607e") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index cf519ed264647ab6d4ee0daee6dec10cd7ee4aa3..7cc744d9e2b5794bc0404bc58774b6147f0a9500 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -72,8 +72,8 @@ Section rules.
     iFrame "Hj". iApply "Hclose". iNext. iExists (<[j:=fill K e']> tp), σ.
     rewrite to_tpool_insert'; last eauto.
     iFrame. iPureIntro.
-    apply rtc_nsteps in Hrtc; destruct Hrtc as [m Hrtc].
-    specialize (Hex HP). apply (nsteps_rtc (m + n)).
+    apply rtc_nsteps_1 in Hrtc; destruct Hrtc as [m Hrtc].
+    specialize (Hex HP). apply (rtc_nsteps_2 (m + n)).
     eapply nsteps_trans; eauto.
     revert e e' Htpj Hex.
     induction n => e e' Htpj Hex.
diff --git a/theories/typing/contextual_refinement_alt.v b/theories/typing/contextual_refinement_alt.v
index c83d34434df58f8bbd8d9513bbfd9bd898677914..e52c6a44f2d90180b97e87f9539c66dac820d8d4 100644
--- a/theories/typing/contextual_refinement_alt.v
+++ b/theories/typing/contextual_refinement_alt.v
@@ -78,7 +78,7 @@ Lemma rtc_erased_step_bot v tp1 tp2 σ1 σ2:
   rtc erased_step (bot #() :: tp1, σ1) (of_val v :: tp2, σ2) →
   False.
 Proof.
-  intros [n Hsteps]%rtc_nsteps. revert tp1 σ1 Hsteps.
+  intros [n Hsteps]%rtc_nsteps_1. revert tp1 σ1 Hsteps.
   induction (lt_wf n) as [n IH1 IH]=>tp1 σ1 Hsteps. destruct n as [|m].
   - inversion Hsteps.
   - inversion Hsteps; simplify_eq/=.