From 3a0d7152c64e329ca7aecbccf020edc355f676be Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 23 Mar 2020 15:23:44 +0100
Subject: [PATCH] Remove redundant space.

---
 theories/program_logic/weakestpre.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 232867fb4..ccbc2e5c2 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -60,7 +60,7 @@ Implicit Types e : expr Λ.
 
 (* Weakest pre *)
 Lemma wp_unfold s E e Φ :
-  WP e @ s; E {{ Φ }} ⊣⊢ wp_pre s (wp (PROP:=iProp Σ)  s) E e Φ.
+  WP e @ s; E {{ Φ }} ⊣⊢ wp_pre s (wp (PROP:=iProp Σ) s) E e Φ.
 Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s)). Qed.
 
 Global Instance wp_ne s E e n :
-- 
GitLab