diff --git a/_CoqProject b/_CoqProject
index 534926fad68657b80605451d958b577091e1cdb5..88e2135fca1cc6bf23ecfe7b06864599bee698df 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -9,7 +9,9 @@
 -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
+-arg -w -arg -notation-overridden 
+# Coq emits warnings when a custom entry is reimported, this is too noisy.
+-arg -w -arg -custom-entry-overriden
 # 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 d3b668f05421b282a875a53d997ccb7d1f3b983b..768f688b8cbed02c6220c1d026d390977e51622e 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -32,6 +32,12 @@ Inductive dfrac :=
   | DfracDiscarded : dfrac
   | DfracBoth : Qp → dfrac.
 
+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 5df0215f54c6ac439cb1b54c50dc5cfe6e8f2a5a..cdee918d3992809fda14774d2d6a394eb7524fb8 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -123,12 +123,6 @@ Section definitions.
 End definitions.
 Arguments meta {L _ _ V Σ _ A _ _} l N x.
 
-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).
-
 Local Notation "l ↦ dq v" := (mapsto l dq v)
   (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
 
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index f40d17bd74dd02e7be931ec47b4d036e7660c393..106b37585743bd53a716c26b46b4354bec66f133 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -47,7 +47,7 @@ Arguments atomic_heap _ {_}.
 
 (** Notation for heap primitives, in a module so you can import it separately. *)
 Module notation.
-otation "l ↦ dq v" := (mapsto l dq v)
+Notation "l ↦ dq v" := (mapsto l dq v)
   (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
 
 Notation "'ref' e" := (alloc e) : expr_scope.
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index 80ac951ce2e9503bae64f9dd9e70e2d68db49f5b..174257263f0237b8275311182e200cb766b43447 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -111,8 +111,8 @@ Section increment.
   (* TODO: Generalize to q and 1-q, based on some theory for a "maybe-mapsto"
      connective that works on [option Qp] (the type of 1-q). *)
   Lemma weak_incr_spec (l: loc) (v : Z) :
-    l ↦{#(1/2)} #v -∗
-    <<< ∀ (v' : Z), l ↦{#(1/2)} #v' >>>
+    l ↦{#1/2} #v -∗
+    <<< ∀ (v' : Z), l ↦{#1/2} #v' >>>
       weak_incr #l @ ⊤
     <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
   Proof.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 4d3c577a92af795a7729b3d8c496cdad6d69ccd6..58c527caa2628452019ac7e1a40078d2830f8ed6 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -28,8 +28,6 @@ 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 ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V))
-  (at level 20) : bi_scope.
 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.
 
@@ -277,7 +275,7 @@ Qed.
 (** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
 value type being [option val]. *)
 
-Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝%Qp.
+Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝.
 Proof. apply mapsto_valid. Qed.
 Lemma mapsto_valid_2 l dq1 dq2 v1 v2 :
   l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.