From f15c614c72f99cb4e74a478c069021fac03e07ca Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Mar 2016 02:37:27 +0100
Subject: [PATCH] Remove superfluous spaces in format of WP.

---
 heap_lang/notation.v       | 2 +-
 program_logic/weakestpre.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 77fa2998f..7632623ff 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -7,7 +7,7 @@ Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
    format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
 Notation "'WP' e {{ Φ } }" := (wp ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
-   format "'WP'  e   {{  Φ  } }") : uPred_scope.
+   format "'WP'  e  {{  Φ  } }") : uPred_scope.
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 6268be63f..f01bb7379 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -62,7 +62,7 @@ Notation "'WP' e @ E {{ Φ } }" := (wp E e Φ)
    format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
 Notation "'WP' e {{ Φ } }" := (wp ⊤ e Φ)
   (at level 20, e, Φ at level 200,
-   format "'WP'  e   {{  Φ  } }") : uPred_scope.
+   format "'WP'  e  {{  Φ  } }") : uPred_scope.
 
 Section wp.
 Context {Λ : language} {Σ : iFunctor}.
-- 
GitLab