From b641e4cf32d390a2ed1c9b6f562d8f1ba9af18c0 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 28 Oct 2017 23:29:02 +0200
Subject: [PATCH] Bump iris, new notation for disjointness.

---
 opam                               | 2 +-
 theories/lifetime/at_borrow.v      | 6 +++---
 theories/lifetime/model/creation.v | 4 ++--
 theories/typing/product.v          | 2 +-
 theories/typing/type.v             | 2 +-
 5 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/opam b/opam
index c5e115a0..660ef8ae 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2017-10-28.3") | (= "dev") }
+  "coq-iris" { (= "dev.2017-10-28.10") | (= "dev") }
 ]
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index b9fef2cf..472f29ff 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 (* TODO : update the TEX with the fact that we can choose the namespace. *)
 Definition at_bor `{invG Σ, lftG Σ} κ N (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗
-    (⌜N ⊥ lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
+    (⌜N ## lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
      ⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
 Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : uPred_scope.
 
@@ -30,7 +30,7 @@ Section atomic_bors.
   Global Instance at_bor_persistent : Persistent (&at{κ, N} P) := _.
 
   Lemma bor_share E κ :
-    N ⊥ lftN → &{κ}P ={E}=∗ &at{κ, N}P.
+    N ## lftN → &{κ}P ={E}=∗ &at{κ, N}P.
   Proof.
     iIntros (HN) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
     iExists i. iFrame "#".
@@ -83,7 +83,7 @@ Section atomic_bors.
   Qed.
 
   Lemma at_bor_fake E κ:
-    ↑lftN ⊆ E → N ⊥ lftN → lft_ctx -∗ [†κ] ={E}=∗ &at{κ,N}P.
+    ↑lftN ⊆ E → N ## lftN → lft_ctx -∗ [†κ] ={E}=∗ &at{κ,N}P.
   Proof.
     iIntros (??) "#LFT#H†". iApply (bor_share with "[>]"); try done.
     by iApply (bor_fake with "LFT H†").
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index c0caed9a..1861dd1b 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -57,7 +57,7 @@ Qed.
 
 Lemma lfts_kill (A : gmap atomic_lft _) (I : gmap lft lft_names) (K K' : gset lft) :
   let Iinv K' := (own_ilft_auth I ∗ [∗ set] κ' ∈ K', lft_inv_alive κ')%I in
-  K ⊥ K' →
+  K ## K' →
   (∀ κ κ', κ ∈ K → is_Some (I !! κ') → κ ⊆ κ' → κ' ∈ K) →
   (∀ κ, lft_alive_in A κ → is_Some (I !! κ) → κ ∉ K → κ ∈ K') →
   Iinv K' -∗ ([∗ set] κ ∈ K, lft_inv A κ ∗ [†κ])
@@ -139,7 +139,7 @@ Proof.
   pose (K' := filter (lft_alive_in A) (dom (gset lft) I) ∖ K).
   destruct (proj1 (subseteq_disjoint_union_L (K ∪ K') (dom (gset lft) I))) as (K''&HI&HK'').
   { set_solver+. }
-  assert (K ⊥ K') by set_solver+.
+  assert (K ## K') by set_solver+.
   rewrite HI !big_sepS_union //. iDestruct "Hinv" as "[[HinvK HinvD] Hinv]".
   iAssert ([∗ set] κ ∈ K', lft_inv_alive κ)%I with "[HinvD]" as "HinvD".
   { iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!#".
diff --git a/theories/typing/product.v b/theories/typing/product.v
index f69b9873..9f92aca2 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -116,7 +116,7 @@ Section product.
     { rewrite <-HF. apply shr_locsE_subseteq. simpl. clear. omega. }
     iMod (@copy_shr_acc with "LFT H2 Htl Htok2") as (q2) "(Htl & H2 & Hclose2)"; first solve_ndisj.
     { move: HF. rewrite /= -plus_assoc shr_locsE_shift.
-      assert (shr_locsE l (ty_size ty1) ⊥ shr_locsE (l +ₗ (ty_size ty1)) (ty_size ty2 + 1))
+      assert (shr_locsE l (ty_size ty1) ## shr_locsE (l +â‚— (ty_size ty1)) (ty_size ty2 + 1))
              by exact: shr_locsE_disj.
       set_solver. }
     iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 2545c45f..a0f6cc6f 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -442,7 +442,7 @@ Section type.
   Qed.
 
   Lemma shr_locsE_disj l n m :
-    shr_locsE l n ⊥ shr_locsE (l +ₗ n) m.
+    shr_locsE l n ## shr_locsE (l +â‚— n) m.
   Proof.
     revert l; induction n; intros l.
     - simpl. set_solver+.
-- 
GitLab