From 68397de6414e8afc5d1ea7dc206d09e01790e984 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 26 Oct 2016 15:35:17 +0200
Subject: [PATCH] Magic updates that take a steps.

---
 program_logic/fancy_updates.v | 6 ++++++
 program_logic/viewshifts.v    | 7 -------
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/program_logic/fancy_updates.v b/program_logic/fancy_updates.v
index 0bde1fff3..f5ed4c41a 100644
--- a/program_logic/fancy_updates.v
+++ b/program_logic/fancy_updates.v
@@ -35,9 +35,15 @@ Notation "P ={ E }=★ Q" := (P ⊢ |={E}=> Q)
 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") : uPred_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") : uPred_scope.
 Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I
   (at level 99, E at level 50, Q at level 200,
    format "|={ E }â–·=>  Q") : uPred_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") : uPred_scope.
 
 Section fupd.
 Context `{irisG Λ Σ}.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index d1cdf24f4..cb8a2c66b 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -20,13 +20,6 @@ Notation "P ={ E }=> Q" := (True ⊢ P ={E}=> Q)%I
   (at level 99, E at level 50, Q at level 200,
    format "P  ={ E }=>  Q") : C_scope.
 
-Notation "P ={ E1 , E2 }â–·=> Q" := (P ={E1,E2}=> â–· |={E2,E1}=> Q)%I
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "P ={ E1 , E2 }â–·=>  Q") : uPred_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") : uPred_scope.
-
 Section vs.
 Context `{irisG Λ Σ}.
 Implicit Types P Q R : iProp Σ.
-- 
GitLab