From 4d09cd406f57e9abc0564f9503510f8e0810f5d2 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 28 Nov 2016 10:10:07 +0100
Subject: [PATCH] Use indexed borrow notation.

---
 theories/lifetime/shr_borrow.v | 2 +-
 theories/lifetime/tl_borrow.v  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 2db70d36..4f5042ef 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/shr_borrow.v
@@ -4,7 +4,7 @@ From lrust.lifetime Require Export derived.
 
 (** Shared bors  *)
 Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
-  (∃ i, idx_bor κ i P ∗ inv lftN (∃ q, idx_bor_own q i))%I.
+  (∃ i, &{κ,i}P ∗ inv lftN (∃ q, idx_bor_own q i))%I.
 Notation "&shr{ κ } P" := (shr_bor κ P)
   (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
 
diff --git a/theories/lifetime/tl_borrow.v b/theories/lifetime/tl_borrow.v
index 34d73141..5770fc4e 100644
--- a/theories/lifetime/tl_borrow.v
+++ b/theories/lifetime/tl_borrow.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
 
 Definition tl_bor `{invG Σ, lftG Σ, thread_localG Σ}
            (κ : lft) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
-  (∃ i, idx_bor κ i P ∗ tl_inv tid N (idx_bor_own 1 i))%I.
+  (∃ i, &{κ,i}P ∗ tl_inv tid N (idx_bor_own 1 i))%I.
 
 Notation "&tl{ κ , tid , N } P" := (tl_bor κ tid N P)
   (format "&tl{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.
-- 
GitLab