diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 3aaa3521ab0ad958666134c36f34e89b241cf6ef..f045dc2c0199cc3d795f572ff61e9f020ec373ff 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -41,11 +41,9 @@ Notation "|==> Q" := (pvs ⊤ ⊤ Q%I)
   (at level 99, Q at level 200, format "|==>  Q") : uPred_scope.
 
 Notation "P ={ E1 , E2 }=> Q" := (P ⊢ |={E1,E2}=> Q)
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }=>  Q") : C_scope.
+  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
 Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
-  (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }=>  Q") : C_scope.
+  (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
 
 Section pvs.
 Context {Λ : language} {Σ : iFunctor}.