From 7709aeaf5f99a43603060a45367870816bd34eea Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 9 Sep 2016 14:39:13 +0200
Subject: [PATCH] Non-primitive VS that take a step.

---
 program_logic/viewshifts.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 02f910142..7fdd6ca05 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -12,6 +12,13 @@ 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.
 
+Notation "P ={ E1 , E2 }â–·=> Q" := (P ={E1%I,E2%I}=> â–· |={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