diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 77fa2998f7f4777d1209e41ae159acfbb80cad79..7632623ff4f85fd54516fc59df2b3f38b5560484 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -7,7 +7,7 @@ Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
    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.
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 6268be63fe2b4055052fe9ef1b1581c6bdb220dc..f01bb7379d76c6c28484f73877e506d4337a80c4 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -62,7 +62,7 @@ Notation "'WP' e @ E {{ Φ } }" := (wp E e Φ)
    format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
 Notation "'WP' e {{ Φ } }" := (wp ⊤ e Φ)
   (at level 20, e, Φ at level 200,
-   format "'WP'  e   {{  Φ  } }") : uPred_scope.
+   format "'WP'  e  {{  Φ  } }") : uPred_scope.
 
 Section wp.
 Context {Λ : language} {Σ : iFunctor}.