From aca9ea1cdd4e8c83ba1cc7f70373b308663c2830 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Jan 2019 19:31:21 +0100
Subject: [PATCH] =?UTF-8?q?bump=20std++=20to=20fix=20and=20test=20=CE=BB..?=
 =?UTF-8?q?=20notation=20printing?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 opam                 |  2 +-
 tests/telescopes.ref | 35 +++++++++++++++++++++++++++++++++++
 tests/telescopes.v   |  9 +++++++++
 3 files changed, 45 insertions(+), 1 deletion(-)

diff --git a/opam b/opam
index 825f04ed6..0b17ee15f 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2019-01-24.0.17241997") | (= "dev") }
+  "coq-stdpp" { (= "dev.2019-01-24.2.b72e1fa8") | (= "dev") }
 ]
diff --git a/tests/telescopes.ref b/tests/telescopes.ref
index 0816c1fa5..5f4957eff 100644
--- a/tests/telescopes.ref
+++ b/tests/telescopes.ref
@@ -13,6 +13,41 @@
   --------------------------------------∗
   |={E2}=> ∃.. x : X, α x ∗ (β x ={E2,E1}=∗ γ2 x)
   
+1 subgoal
+  
+  PROP : sbi
+  BiFUpd0 : BiFUpd PROP
+  X : tele
+  E1, E2 : coPset
+  α, β, γ1, γ2 : X → PROP
+  ============================
+  accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β (λ.. x : X, γ1 x ∨ γ2 x)
+1 subgoal
+  
+  PROP : sbi
+  BiFUpd0 : BiFUpd PROP
+  X : tele
+  E1, E2 : coPset
+  α, β, γ1, γ2 : X → PROP
+  x : X
+  ============================
+  "Hγ1" : γ1 x
+  --------------------------------------∗
+  (λ.. x0 : X, γ1 x0 ∨ γ2 x0) x
+  
+1 subgoal
+  
+  PROP : sbi
+  BiFUpd0 : BiFUpd PROP
+  X : tele
+  E1, E2 : coPset
+  α, β, γ1, γ2 : X → PROP
+  x : X
+  ============================
+  "Hγ1" : γ1 x
+  --------------------------------------∗
+  γ1 x ∨ γ2 x
+  
 1 subgoal
   
   PROP : sbi
diff --git a/tests/telescopes.v b/tests/telescopes.v
index 621e086df..a60ba91e0 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -33,6 +33,15 @@ Proof.
   iModIntro. iExists x'. iFrame. iIntros "Hβ".
   iMod ("Hclose" with "Hβ") as "Hγ". iApply "Hγ12". auto.
 Qed.
+
+Lemma acc_mono_disj E1 E2 α β γ1 γ2 :
+  accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β (λ.. x, γ1 x ∨ γ2 x).
+Proof.
+  Show.
+  iApply acc_mono. iIntros (x) "Hγ1". Show.
+  rewrite ->tele_app_bind. Show.
+  iLeft. done.
+Qed.
 End tests.
 
 Section printing_tests.
-- 
GitLab