diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index c64497696378ea0d59c8adc2d970b770d3784abe..d522114bde58578c7a603f55f7b5d02fa86fe3e1 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -90,6 +90,9 @@ Reserved Notation "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,
    format "|={ E1 , E2 }â–·=>^ n  Q").
+Reserved Notation "P ={ E1 , E2 }▷=∗^ n Q"
+  (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
+   format "P  ={ E1 , E2 }▷=∗^ n  Q").
 
 (** Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 40a3437b4ed349cd07759d2c67705009b082c306..f36e712e15b35edf52a60c4a45e47f3181fb98d0 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -33,6 +33,8 @@ Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2, E1 }▷=> Q)%I : bi_s
 Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I : bi_scope.
 Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I : bi_scope.
 Notation "|={ E1 , E2 }▷=>^ n Q" := (Nat.iter n (λ P, |={E1,E2}▷=> P) Q)%I : bi_scope.
+Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P ⊢ |={E1,E2}▷=>^n Q)%I (only parsing) : stdpp_scope.
+Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P -∗ |={E1,E2}▷=>^n Q)%I : bi_scope.
 
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)