diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 7960c20a4d85254d5cdeb31598b02f9cc109fa27..aacf160c5cfb2eb222f72709bae11e84718db7d6 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -221,19 +221,6 @@ Hint Extern 2 (coq_tactics.envs_entails _ (|={_}=> _)) => iModIntro.
 
 (** Fancy updates that take a step. *)
 
-Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 }â–·=>  Q") : bi_scope.
-Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2 }▷=> Q)%I
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }▷=∗  Q") : bi_scope.
-Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I
-  (at level 99, E at level 50, Q at level 200,
-   format "|={ E }â–·=>  Q") : bi_scope.
-Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I
-  (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }▷=∗  Q") : bi_scope.
-
 Section step_fupd.
 Context `{invG Σ}.
 
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 12a4558b050214a1aee5af5328b6cffee80a98d3..e4bc4e09184429ddd542b74a5f8dc0007401aba2 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -31,3 +31,18 @@ Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
    format "P  ={ E }=∗  Q") : bi_scope.
 Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
   (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
+
+(** Fancy updates that take a step. *)
+
+Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "|={ E1 , E2 }â–·=>  Q") : bi_scope.
+Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2 }▷=> Q)%I
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }▷=∗  Q") : bi_scope.
+Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "|={ E }â–·=>  Q") : bi_scope.
+Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }▷=∗  Q") : bi_scope.