diff --git a/theories/heap_lang/locations.v b/theories/heap_lang/locations.v
index dd2a48a3d3a85e00a1b29fb65002127f6c9606a9..b751bc1ebb33b9e71bf797eba2b77a5dd74de1f2 100644
--- a/theories/heap_lang/locations.v
+++ b/theories/heap_lang/locations.v
@@ -18,7 +18,8 @@ Next Obligation. done. Qed.
 Definition loc_add (l : loc) (off : Z) : loc :=
   {| loc_car := loc_car l + off|}.
 
-Notation "l +â‚— off" := (loc_add l off) (at level 50, left associativity).
+Notation "l +â‚— off" :=
+  (loc_add l off) (at level 50, left associativity) : stdpp_scope.
 
 Lemma loc_add_assoc l i j : l +â‚— i +â‚— j = l +â‚— (i + j).
 Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index ae3d54943398868d220d02a885f142349408b181..204ec38ab76de2a755935bfdb13ef8a68350bb96 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -32,7 +32,7 @@ Notation Skip := (App (Val $ LamV BAnon (Val $ LitV LitUnit)) (Val $ LitV LitUni
 
 (* No scope for the values, does not conflict and scope is often not inferred
 properly. *)
-Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
+Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l").
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)