From b91a628094ba03128b37e1e3a7b4bc6bdfaffad1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 21 May 2016 12:31:11 +0200
Subject: [PATCH] proofmode: add test for mask-changing view shift

---
 tests/proofmode.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 8146ab115..d7431c406 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,4 +1,5 @@
 From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import pviewshifts.
 
 Lemma demo_0 {M : cmraT} (P Q : uPred M) :
   □ (P ∨ Q) ⊢ ((∀ x, x = 0 ∨ x = 1) → (Q ∨ P)).
@@ -79,3 +80,16 @@ Proof.
   iIntros "#Hfoo **".
   by iIntros "# _".
 Qed.
+
+Section iris.
+  Context {Λ : language} {Σ : iFunctor}.
+
+  Lemma demo_7 (E1 E2 E : coPset) (P : iProp Λ Σ) :
+    E1 ⊆ E2 → E ⊆ E1 →
+    (|={E1,E}=> ▷ P) ⊢ (|={E2,E ∪ E2 ∖ E1}=> ▷ P).
+  Proof.
+    iIntros {? ?} "Hpvs".
+    iPvs "Hpvs"; first (split_and?; set_solver).
+    done.
+  Qed.
+End iris.
-- 
GitLab