From 69b10ed1b5857efdfda2847ec139bd24c7611b56 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 8 Sep 2016 01:01:55 +0200
Subject: [PATCH] Notation for primitive view shifts that take a step.

---
 program_logic/pviewshifts.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 586777c6f..daf4eb7f1 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -34,6 +34,9 @@ Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
 Notation "|={ E1 , E2 }â–·=> Q" := (|={E1%I,E2%I}=> â–· |={E2,E1}=> Q)%I
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ 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.
 
 Section pvs.
 Context `{irisG Λ Σ}.
-- 
GitLab