diff --git a/semantics.opam b/semantics.opam
index 05534f25b1573a0c459e26cac589a7d74efa1859..54e76fda91ae4af548a513645642852cc541d990 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -10,7 +10,7 @@ version: "dev"
 
 depends: [
   "coq" { (>= "8.20" & < "8.21~") | (= "dev") }
-  "coq-iris-heap-lang" { (= "dev.2024-12-06.1.72e683c9") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2025-02-27.1.c773500a") | (= "dev") }
   "coq-equations" { (= "1.3.1+8.20") }
   "coq-autosubst" { (= "1.9") | (= "dev") }
 ]
diff --git a/theories/program_logics/program_logic/notation.v b/theories/program_logics/program_logic/notation.v
index 88b18556532d85224f23e8b2d853272cf2155d1c..5f32211ae102673a27a1c1009b9a214c6b40fd14 100644
--- a/theories/program_logics/program_logic/notation.v
+++ b/theories/program_logics/program_logic/notation.v
@@ -43,27 +43,26 @@ Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ ⊤ e%E Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
 
 Notation "'WP' e @ s ; E1 ; E2 {{ v , Q } }" := (wp s E1 E2 e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
+  (at level 20, e, Q at level 200, v at level 200 as pattern,
    format "'[hv' 'WP'  e  '/' @  '[' s ;  '/' E1 ;  '/' E2  ']' '/' {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
 Notation "'WP' e @ E1 ; E2 {{ v , Q } }" := (wp NotStuck E1 E2 e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
+  (at level 20, e, Q at level 200, v at level 200 as pattern,
    format "'[hv' 'WP'  e  '/' @  '[' E1 ;  '/' E2  ']' '/' {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
 Notation "'WP' e @ E1 ; E2 ? {{ v , Q } }" := (wp MaybeStuck E1 E2 e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
+  (at level 20, e, Q at level 200, v at level 200 as pattern,
    format "'[hv' 'WP'  e  '/' @  '[' E1 ;  '/' E2  ']'  '/' ? {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
 Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E E e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
+  (at level 20, e, Q at level 200, v at level 200 as pattern,
    format "'[hv' 'WP'  e  '/' @  '[' s ;  '/' E  ']' '/' {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
 Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck E E e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
+  (at level 20, e, Q at level 200, v at level 200 as pattern,
    format "'[hv' 'WP'  e  '/' @  E  '/' {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
 Notation "'WP' e @ E ? {{ v , Q } }" := (wp MaybeStuck E E e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
+  (at level 20, e, Q at level 200, v at level 200 as pattern,
    format "'[hv' 'WP'  e  '/' @  E  '/' ? {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
 Notation "'WP' e {{ v , Q } }" := (wp NotStuck ⊤ ⊤ e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
+  (at level 20, e, Q at level 200, v at level 200 as pattern,
    format "'[hv' 'WP'  e  '/' {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
 Notation "'WP' e ? {{ v , Q } }" := (wp MaybeStuck ⊤ ⊤ e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
+  (at level 20, e, Q at level 200, v at level 200 as pattern,
    format "'[hv' 'WP'  e  '/' ? {{  '[' v ,  '/' Q  ']' } } ']'") : bi_scope.
-