Move fancy updates that take a step in bi/

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 Σ}.
 

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.