From 260e8ecd81c7bb528079736f40ef641f1afb010d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 9 Nov 2019 09:50:35 +0100
Subject: [PATCH] Remove spurious space.

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

diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 47789deb9..97df3d632 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -213,7 +213,7 @@ Proof.
 Qed.
 
 Lemma into_wand_monPred_at_unknown_unknown p q R P 𝓟 Q 𝓠 i :
-  IntoWand p q R P Q →  MakeMonPredAt i P 𝓟 → MakeMonPredAt i Q 𝓠 →
+  IntoWand p q R P Q → MakeMonPredAt i P 𝓟 → MakeMonPredAt i Q 𝓠 →
   IntoWand p q (R i) 𝓟 𝓠.
 Proof.
   rewrite /IntoWand /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
-- 
GitLab