diff --git a/program_logic/upred.v b/program_logic/upred.v
index 7bafefba9453dbddd20bda856ae98f69f170d1ed..12df00e7aeae21ab5ee77bf0ccab6b06c9611936 100644
--- a/program_logic/upred.v
+++ b/program_logic/upred.v
@@ -208,7 +208,7 @@ Arguments uPred_holds {_} _%I _ _.
 Arguments uPred_entails _ _%I _%I.
 Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
 Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
-Notation "■ φ" := (uPred_const φ) (at level 20) : uPred_scope.
+Notation "■ φ" := (uPred_const φ%type) (at level 20) : uPred_scope.
 Notation "'False'" := (uPred_const False) : uPred_scope.
 Notation "'True'" := (uPred_const True) : uPred_scope.
 Infix "∧" := uPred_and : uPred_scope.