diff --git a/algebra/upred.v b/algebra/upred.v
index 76846af48e2d9f8b64ef123f1aef9f94be1ece4e..1005bf06fa78508d558d70aea253394f0d9d844a 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -286,7 +286,7 @@ Infix "→" := uPred_impl : uPred_scope.
 Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
 Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
 Notation "P -★ Q" := (uPred_wand P Q)
-  (at level 199, Q at level 200, right associativity) : uPred_scope.
+  (at level 99, Q at level 200, right associativity) : uPred_scope.
 Notation "∀ x .. y , P" :=
   (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
 Notation "∃ x .. y , P" :=