Bump iris, new notation for disjointness.

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") }
 ]

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†").

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 "!#".

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]".

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+.