diff --git a/semantics.opam b/semantics.opam
index 6324efb19135e2c8a8787acb1a9c16c7dc9837c2..19d4d90cbaa7fdb58aef034ea2ead4f69bdc0050 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -10,7 +10,7 @@ version: "dev"
 
 depends: [
   "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
-  "coq-iris-heap-lang" { (= "dev.2022-11-24.2.5b5d3f4d") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2022-11-29.2.de908f52") | (= "dev") }
   "coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15")  | (= "1.3+8.16") }
   "coq-autosubst" { (= "1.7") | (= "dev")  }
 ]
diff --git a/theories/program_logics/program_logic/adequacy.v b/theories/program_logics/program_logic/adequacy.v
index 07c035e698d46ca5e7a8664dd2284d65618dfdd3..499558fc701ae75557c60e062dbdf3c35e25b45e 100644
--- a/theories/program_logics/program_logic/adequacy.v
+++ b/theories/program_logics/program_logic/adequacy.v
@@ -145,6 +145,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invGpreS Σ} e σ1 n κs t2 σ2 φ :
   φ.
 Proof.
   intros Hwp ?.
+  eapply pure_soundness.
   apply (step_fupdN_soundness_no_lc _ n 0)=> Hinv.
   iIntros "_".
   iMod Hwp as (s stateI Φ) "(Hσ & Hwp & Hφ)".