remove unnecessary space in inv_mapsto_own notation

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

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