From e9ac097ae9f0326271e10aa3715a8a28e5bc52ba Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 15 Dec 2017 15:37:45 +0100
Subject: [PATCH] Move fancy updates that take a step in bi/

---
 theories/base_logic/lib/fancy_updates.v | 13 -------------
 theories/bi/updates.v                   | 15 +++++++++++++++
 2 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 7960c20a4..aacf160c5 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 12a4558b0..e4bc4e091 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.
-- 
GitLab