diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 4a8dd7f516c9c0f786e2d6e4fe301c220efdde62..c64497696378ea0d59c8adc2d970b770d3784abe 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -88,7 +88,8 @@ Reserved Notation "P ={ E }▷=∗ Q"
   (at level 99, E at level 50, Q at level 200,
    format "'[' P  '/' ={ E }▷=∗  Q ']'").
 Reserved Notation "|={ E1 , E2 }â–·=>^ n Q"
-  (at level 99, E1, E2 at level 50, n at level 9, Q at level 200).
+  (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
+   format "|={ E1 , E2 }â–·=>^ n  Q").
 
 (** Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"