diff --git a/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v
index 0031b43bd0a76a6a5dbbaf2096e6d4715f1918f2..a6fd87779a71487bf25ace21e3ef80687d0a2b80 100644
--- a/theories/base_logic/lib/gen_inv_heap.v
+++ b/theories/base_logic/lib/gen_inv_heap.v
@@ -71,7 +71,7 @@ End definitions.
 Local Notation "l '↦□' I" := (inv_mapsto l I%stdpp%type)
   (at level 20, format "l  '↦□'  I") : bi_scope.
 
-Local Notation "l '↦_' I  v" := (inv_mapsto_own l v I%stdpp%type)
+Local Notation "l '↦_' I v" := (inv_mapsto_own l v I%stdpp%type)
   (at level 20, I at level 9, format "l  '↦_' I  v") : bi_scope.
 
 (* [inv_heap_inv] has no parameters to infer the types from, so we need to
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 1fd614dc81da5fffe679edca4e3017f93404461e..814e86d99634ffa1b1c067162d916b9f5684d3c1 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -33,7 +33,7 @@ Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 
 Notation "l ↦□ I" := (inv_mapsto (L:=loc) (V:=val) l I%stdpp%type)
   (at level 20, format "l  ↦□  I") : bi_scope.
-Notation "l ↦_ I  v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type)
+Notation "l ↦_ I v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type)
   (at level 20, I at level 9, format "l  ↦_ I   v") : bi_scope.
 
 (** The tactic [inv_head_step] performs inversion on hypotheses of the shape