From 6dba682d679ff5b84e10c4828c9f090c9416ad67 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 18 Apr 2020 22:12:49 +0200
Subject: [PATCH] remove unnecessary space in inv_mapsto_own notation

---
 theories/base_logic/lib/gen_inv_heap.v | 2 +-
 theories/heap_lang/lifting.v           | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v
index 0031b43bd..a6fd87779 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 1fd614dc8..814e86d99 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
-- 
GitLab