diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index 27896d8d2c0fb0e6ef70423949eddcca8532ed82..299d9cd302d32367360ce69689d21d40e649e4cb 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -190,7 +190,7 @@ Notation "P ==∗ Q" := (P -∗ |==> Q)%I
 
 Coercion uPred_valid {M} (P : uPred M) : Prop := True%I ⊢ P.
 Notation "P -∗ Q" := (P ⊢ Q)
-  (at level 99, Q at level 200, right associativity, only parsing) : C_scope.
+  (at level 99, Q at level 200, right associativity) : C_scope.
 
 Module uPred_primitive.
 Definition unseal :=