From 21ceb92f0b829201c24ce02f8981b7fe29f29304 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Mar 2016 02:38:18 +0100
Subject: [PATCH] Notation for pvs with full mask.

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

diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index b56fa5470..6a2516c92 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -38,6 +38,8 @@ Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
 Notation "|={ E }=> Q" := (pvs E E Q%I)
   (at level 199, E at level 50, Q at level 200,
    format "|={ E }=>  Q") : uPred_scope.
+Notation "|==> Q" := (pvs ⊤ ⊤ Q%I)
+  (at level 199, Q at level 200, format "|==>  Q") : uPred_scope.
 
 Section pvs.
 Context {Λ : language} {Σ : iFunctor}.
-- 
GitLab