diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index b0c41722382417821adb1537a3db65f8f91065b3..41c7652b25021e29bdafe5fff15b70d8ae7ae198 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -123,6 +123,8 @@ Section definitions.
 End definitions.
 Arguments meta {L _ _ V Σ _ A _ _} l N x.
 
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Local Notation "l ↦{ dq } v" := (mapsto l dq v)
   (at level 20, format "l  ↦{ dq }  v") : bi_scope.
 Local Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index b0bfdf89cc71ac1a961a1c34df083237ae49334d..72ce1856a03c5ceff3499ddfcdb43719a8538daf 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -16,6 +16,9 @@ with lists of values. *)
 
 Definition array `{!heapG Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
   ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{dq} v)%I.
+
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Notation "l ↦∗{ dq } vs" := (array l dq vs)
   (at level 20, format "l  ↦∗{ dq }  vs") : bi_scope.
 Notation "l ↦∗□ vs" := (array l DfracDiscarded vs)
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 5b3c1c802b58d0f896d9dcded6a697bd16ce2395..85255d1272e8bdb04839c389477127e592ff5a6e 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -48,21 +48,23 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
 Arguments atomic_heap _ {_}.
 
 (** Notation for heap primitives, in a module so you can import it separately. *)
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Module notation.
-Notation "l ↦{ dq } v" := (mapsto l dq v)
-  (at level 20, format "l  ↦{ dq }  v") : bi_scope.
-Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
-  (at level 20, format "l  ↦□  v") : bi_scope.
-Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
-  (at level 20, format "l  ↦{# q }  v") : bi_scope.
-Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
-  (at level 20, format "l  ↦  v") : bi_scope.
-
-Notation "'ref' e" := (alloc e) : expr_scope.
-Notation "! e" := (load e) : expr_scope.
-Notation "e1 <- e2" := (store e1 e2) : expr_scope.
-
-Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
+  Notation "l ↦{ dq } v" := (mapsto l dq v)
+    (at level 20, format "l  ↦{ dq }  v") : bi_scope.
+  Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
+    (at level 20, format "l  ↦□  v") : bi_scope.
+  Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
+    (at level 20, format "l  ↦{# q }  v") : bi_scope.
+  Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
+    (at level 20, format "l  ↦  v") : bi_scope.
+
+  Notation "'ref' e" := (alloc e) : expr_scope.
+  Notation "! e" := (load e) : expr_scope.
+  Notation "e1 <- e2" := (store e1 e2) : expr_scope.
+
+  Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
 
 End notation.
 
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index e2ef9e733387be33a46adc0bd4800c4d91d9e3ad..0f168abe0db1c3653d00d26d89edb7a6693bd112 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -28,6 +28,8 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
 
 (** Since we use an [option val] instance of [gen_heap], we need to overwrite
 the notations.  That also helps for scopes and coercions. *)
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Notation "l ↦{ dq } v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V))
   (at level 20, format "l  ↦{ dq }  v") : bi_scope.
 Notation "l ↦□ v" := (mapsto (L:=loc) (V:=option val) l DfracDiscarded (Some v%V))