From f7f0a171b38c358e85211bd6b67f1469a8efbd82 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 30 Jan 2020 14:20:14 +0100
Subject: [PATCH] Add space.

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

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 39e86c98d..ee4335b04 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -82,7 +82,7 @@ Section cofe.
   Canonical Structure uPredO : ofeT := OfeT (uPred M) uPred_ofe_mixin.
 
   Program Definition uPred_compl : Compl uPredO := λ c,
-    {| uPred_holds n x := ∀ n', n' ≤ n → ✓{n'}x → c n' n' x |}.
+    {| uPred_holds n x := ∀ n', n' ≤ n → ✓{n'} x → c n' n' x |}.
   Next Obligation.
     move=> /= c n1 n2 x1 x2 HP Hx12 Hn12 n3 Hn23 Hv. eapply uPred_mono.
     eapply HP, cmra_validN_includedN, cmra_includedN_le=>//; lia.
-- 
GitLab