diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 39e86c98dc99919c2a32fe7828bd6a5ef1438177..ee4335b0427c8f123f5d3d19a1e3ead974eb59c4 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.