diff --git a/_CoqProject b/_CoqProject
index 88e2135fca1cc6bf23ecfe7b06864599bee698df..534926fad68657b80605451d958b577091e1cdb5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -9,9 +9,7 @@
 -Q iris/program_logic iris.program_logic
 -Q iris_heap_lang iris.heap_lang
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
--arg -w -arg -notation-overridden 
-# Coq emits warnings when a custom entry is reimported, this is too noisy.
--arg -w -arg -custom-entry-overriden
+-arg -w -arg -notation-overridden
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index 63ab13fc17c5f1272102512cbc3788badb1414f4..d3b668f05421b282a875a53d997ccb7d1f3b983b 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -32,16 +32,6 @@ Inductive dfrac :=
   | DfracDiscarded : dfrac
   | DfracBoth : Qp → dfrac.
 
-(* This notation is intended to be used as a component in other notations that
-   include discardable fractions. The notation provides shorthands for the
-   constructors and the commonly used full fraction. For an example
-   demonstrating how this can be used see the notation in [gen_heap.v]. *)
-Declare Custom Entry dfrac.
-Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
-Notation "â–¡" := DfracDiscarded (in custom dfrac).
-Notation "{# q }" := (DfracOwn q) (in custom dfrac at level 1, q constr).
-Notation "" := (DfracOwn 1) (in custom dfrac).
-
 Section dfrac.
   Canonical Structure dfracO := leibnizO dfrac.
 
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 99e96611dd50c225a5d7576eaa5a2924cd5fa3a3..b0c41722382417821adb1537a3db65f8f91065b3 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -123,8 +123,14 @@ Section definitions.
 End definitions.
 Arguments meta {L _ _ V Σ _ A _ _} l N x.
 
-Local Notation "l ↦ dq v" := (mapsto l dq v)
-  (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
+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)
+  (at level 20, format "l  ↦□  v") : bi_scope.
+Local Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
+  (at level 20, format "l  ↦{# q }  v") : bi_scope.
+Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
+  (at level 20, format "l  ↦  v") : bi_scope.
 
 Section gen_heap.
   Context {L V} `{Countable L, !gen_heapG L V Σ}.
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index c4fe31053359b4db23244fc79300a15ee617569a..b0bfdf89cc71ac1a961a1c34df083237ae49334d 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -16,8 +16,14 @@ with lists of values. *)
 
 Definition array `{!heapG Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
   ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{dq} v)%I.
-Notation "l ↦∗ dq vs" := (array l dq vs)
-  (at level 20, dq custom dfrac  at level 1, format "l  ↦∗ dq  vs") : bi_scope.
+Notation "l ↦∗{ dq } vs" := (array l dq vs)
+  (at level 20, format "l  ↦∗{ dq }  vs") : bi_scope.
+Notation "l ↦∗□ vs" := (array l DfracDiscarded vs)
+  (at level 20, format "l  ↦∗□  vs") : bi_scope.
+Notation "l ↦∗{# q } vs" := (array l (DfracOwn q) vs)
+  (at level 20, format "l  ↦∗{# q }  vs") : bi_scope.
+Notation "l ↦∗ vs" := (array l (DfracOwn 1) vs)
+  (at level 20, format "l  ↦∗  vs") : bi_scope.
 
 (** We have [FromSep] and [IntoSep] instances to split the fraction (via the
 [AsFractional] instance below), but not for splitting the list, as that would
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 62edb1d2cf47147a778551e4fa31d9b16b6039e5..5b3c1c802b58d0f896d9dcded6a697bd16ce2395 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -49,8 +49,14 @@ Arguments atomic_heap _ {_}.
 
 (** Notation for heap primitives, in a module so you can import it separately. *)
 Module notation.
-Notation "l ↦ dq v" := (mapsto l dq v)
-  (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
+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.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 58c527caa2628452019ac7e1a40078d2830f8ed6..e2ef9e733387be33a46adc0bd4800c4d91d9e3ad 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -28,8 +28,14 @@ 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. *)
-Notation "l ↦ dq v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V))
-  (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
+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))
+  (at level 20, format "l  ↦□  v") : bi_scope.
+Notation "l ↦{# q } v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn q) (Some v%V))
+  (at level 20, format "l  ↦{# q }  v") : bi_scope.
+Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V))
+  (at level 20, format "l  ↦  v") : bi_scope.
 
 (** Same for [gen_inv_heap], except that these are higher-order notations so to
 make setoid rewriting in the predicate [I] work we need actual definitions