diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 2b6cf0f47f34f565540b9c25ddc10157308b2773..23235b3c8a509a349a1748af4eaba650834d8c93 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -40,17 +40,17 @@ Instance: Params (@wp) 5.
 
 Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
   (at level 20, e, Φ at level 200,
-   format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
+   format "'[' 'WP'  e  '/' @  E  {{  Φ  } } ']'") : uPred_scope.
 Notation "'WP' e {{ Φ } }" := (wp ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
-   format "'WP'  e  {{  Φ  } }") : uPred_scope.
+   format "'[' 'WP'  e  '/' {{  Φ  } } ']'") : uPred_scope.
 
 Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'WP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
+   format "'[' 'WP'  e  '/' @  E  {{  v ,  Q  } } ']'") : uPred_scope.
 Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
+   format "'[' 'WP'  e  '/' {{  v ,  Q  } } ']'") : uPred_scope.
 
 (* Texan triples *)
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=