From 59f2c74ce4d9500fc3d7eb3090801d383b89c2b6 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 25 May 2018 20:29:51 +0200
Subject: [PATCH] Change names for bor_persistent.

---
 theories/lifetime/lifetime.v                       | 6 +++---
 theories/typing/borrow.v                           | 2 +-
 theories/typing/lib/arc.v                          | 6 +++---
 theories/typing/lib/mutex/mutexguard.v             | 8 ++++----
 theories/typing/lib/rc/rc.v                        | 2 +-
 theories/typing/lib/rc/weak.v                      | 2 +-
 theories/typing/lib/refcell/ref.v                  | 8 ++++----
 theories/typing/lib/refcell/refmut.v               | 4 ++--
 theories/typing/lib/refcell/refmut_code.v          | 4 ++--
 theories/typing/lib/rwlock/rwlockreadguard.v       | 8 ++++----
 theories/typing/lib/rwlock/rwlockwriteguard.v      | 4 ++--
 theories/typing/lib/rwlock/rwlockwriteguard_code.v | 4 ++--
 theories/typing/own.v                              | 2 +-
 theories/typing/type.v                             | 2 +-
 theories/typing/uniq_bor.v                         | 2 +-
 15 files changed, 32 insertions(+), 32 deletions(-)

diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index a05aa8af..22ba7677 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -119,7 +119,7 @@ Proof.
   iModIntro. iNext. iApply ("Hclose" with "[] HP"). by iIntros "!> $".
 Qed.
 
-Lemma bor_persistent P `{!Persistent P} E κ :
+Lemma bor_persistent_notok P `{!Persistent P} E κ :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P ={E}=∗ ▷ P ∨ [†κ].
 Proof.
@@ -129,7 +129,7 @@ Proof.
   - iMod "Hclose" as "_". auto.
 Qed.
 
-Lemma bor_persistent_tok P `{!Persistent P} E κ q :
+Lemma bor_persistent P `{!Persistent P} E κ q :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
 Proof.
@@ -174,7 +174,7 @@ Proof.
   rewrite ->(bor_unfold_idx _ P).
   iMod (bor_exists with "LFT Hbor") as (i) "Hbor"; [done|].
   iMod (bor_sep with "LFT Hbor") as "[Hidx Hbor]"; [done|].
-  iMod (bor_persistent with "LFT Hidx") as "#[Hidx|H†]"; [done| |].
+  iMod (bor_persistent_notok with "LFT Hidx") as "#[Hidx|H†]"; [done| |].
   - iIntros "!>". iNext. by iApply (idx_bor_unnest with "LFT Hidx Hbor").
   - iApply (bor_fake with "LFT"); [done|]. rewrite -lft_dead_or. auto.
 Qed.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 33a26116..680dca38 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -151,7 +151,7 @@ Section borrow.
     iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
     iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
     destruct vl as [|[[]|][]];
-      try by iMod (bor_persistent_tok with "LFT Hbor Htok") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT Hbor Htok") as "[>[] _]".
     iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
     rewrite heap_mapsto_vec_singleton.
     iMod (bor_unnest with "LFT Hbor") as "Hbor"; [done|].
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index afbdf5cb..ce484f17 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -116,7 +116,7 @@ Section arc.
        but that would be additional work here... *)
     iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
     destruct vl as [|[[|l'|]|][|]];
-      try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
     setoid_rewrite heap_mapsto_vec_singleton.
     iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
     iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
@@ -237,7 +237,7 @@ Section arc.
        but that would be additional work here... *)
     iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
     destruct vl as [|[[|l'|]|][|]];
-      try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
     setoid_rewrite heap_mapsto_vec_singleton.
     iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
     iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
@@ -934,7 +934,7 @@ Section arc.
     iMod (bor_exists with "LFT Hrc'") as (rcvl) "Hrc'"=>//.
     iMod (bor_sep with "LFT Hrc'") as "[Hrc'↦ Hrc]"=>//.
     destruct rcvl as [|[[|rc|]|][|]]; try by
-      iMod (bor_persistent_tok with "LFT Hrc Hα") as "[>[] ?]".
+      iMod (bor_persistent with "LFT Hrc Hα") as "[>[] ?]".
     rewrite heap_mapsto_vec_singleton.
     iMod (bor_acc with "LFT Hrc'↦ Hα") as "[Hrc'↦ Hclose2]"=>//. wp_read.
     iMod ("Hclose2" with "Hrc'↦") as "[_ Hα]".
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index d28626c9..507f88e0 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -51,12 +51,12 @@ Section mguard.
     iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done.
     iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
     destruct vl as [|[[|l'|]|][]];
-      try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
     setoid_rewrite heap_mapsto_vec_singleton.
     iMod (bor_exists with "LFT Hb") as (β) "Hb"; first done.
     iMod (bor_sep with "LFT Hb") as "[Hαβ H]"; first done.
     iMod (bor_sep with "LFT H") as "[_ H]"; first done.
-    iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]"; first done.
+    iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]"; first done.
     iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
     (* FIXME: "iApply lft_intersect_mono" only preserves the later on the last
        goal, as does "iApply (lft_intersect_mono with ">")". *)
@@ -208,12 +208,12 @@ Section code.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)";
       [solve_typing..|].
     destruct vl as [|[[|lm|]|] [|]]; simpl;
-      try by iMod (bor_persistent_tok with "LFT Hprot Hα") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT Hprot Hα") as "[>[] _]".
     rewrite heap_mapsto_vec_singleton.
     iMod (bor_exists with "LFT Hprot") as (κ) "Hprot"; first done.
     iMod (bor_sep with "LFT Hprot") as "[Hβκ Hprot]"; first done.
     iMod (bor_sep with "LFT Hprot") as "[_ Hlm]"; first done.
-    iMod (bor_persistent_tok with "LFT Hβκ Hα") as "[#Hβκ Hα]"; first done.
+    iMod (bor_persistent with "LFT Hβκ Hα") as "[#Hβκ Hα]"; first done.
     iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hclose2]"; first done.
     wp_bind (!_)%E. iMod (bor_unnest with "LFT Hlm") as "Hlm"; first done.
     wp_read. wp_let. iMod "Hlm".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index c798b046..2ab6d344 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -135,7 +135,7 @@ Section rc.
     iMod (bor_sep with "LFT Hb") as "[H↦ Hb]"; first done.
     iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
     destruct vl as [|[[|l'|]|][|]];
-      try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
     setoid_rewrite heap_mapsto_vec_singleton.
     iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
     iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index ed05e2e2..291c57a7 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -33,7 +33,7 @@ Section weak.
        but that would be additional work here... *)
     iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
     destruct vl as [|[[|l'|]|][|]];
-      try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
     setoid_rewrite heap_mapsto_vec_singleton.
     iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
     iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index dfa8aec0..d5307a39 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -42,18 +42,18 @@ Section ref.
     iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
     iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
     destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
-      try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
     iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (q') "Hb". done.
     iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (ty') "Hb". done.
     iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". done.
-    iMod (bor_persistent_tok with "LFT Hshr Htok") as "[#Hshr Htok]". done.
+    iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]". done.
     iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". done.
-    iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
+    iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
     iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
-    iMod (bor_persistent_tok with "LFT Hinv Htok") as "[#Hinv $]". done.
+    iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]". done.
     iMod (bor_sep with "LFT Hb") as "[Hκν Hb]". done.
     iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
     { iApply bor_fracture; try done. by rewrite Qp_mult_1_r. }
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 9cc32a04..f9a2ec91 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -43,7 +43,7 @@ Section refmut.
     iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
     iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
     destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
-      try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
     iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
@@ -55,7 +55,7 @@ Section refmut.
     { by rewrite Qp_mult_1_l. }
     iDestruct (frac_bor_lft_incl _ _ 1 with "LFT H") as "#Hκν". iClear "H".
     iMod (bor_sep with "LFT Hb") as "[Hb Hαβ]". done.
-    iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
+    iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
     iExists _, _. iFrame "H↦". iApply delay_sharing_nested; try done.
     rewrite -assoc. iApply lft_intersect_mono; first by iApply lft_incl_refl.
     iApply lft_incl_glb; first done. iApply lft_incl_refl.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index ccb739e1..e2f0360b 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -71,14 +71,14 @@ Section refmut_functions.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose')";
       [solve_typing..|].
     destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
-      try by iMod (bor_persistent_tok with "LFT H Hα") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT H Hα") as "[>[] _]".
     iMod (bor_exists with "LFT H") as (ν) "H". done.
     iMod (bor_exists with "LFT H") as (γ) "H". done.
     iMod (bor_exists with "LFT H") as (δ) "H". done.
     iMod (bor_exists with "LFT H") as (ty') "H". done.
     iMod (bor_sep with "LFT H") as "[Hb H]". done.
     iMod (bor_sep with "LFT H") as "[Hβδ H]". done.
-    iMod (bor_persistent_tok with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
+    iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
     rewrite (comm _ (1).[ν])%I. rewrite (assoc _ _ _ (1).[ν])%I.
     iMod (bor_sep with "LFT H") as "[_ H]". done.
     iMod (bor_fracture (λ q, (1 * q).[ν])%I with "LFT [H]") as "H". done.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 1beca19d..1b0ffdc5 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -37,17 +37,17 @@ Section rwlockreadguard.
     iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
     iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
     destruct vl as [|[[|l'|]|][]];
-      try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
     iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (q') "Hb". done.
     iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
     iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". done.
-    iMod (bor_persistent_tok with "LFT Hshr Htok") as "[#Hshr Htok]". done.
+    iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]". done.
     iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". done.
-    iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
+    iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
     iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
-    iMod (bor_persistent_tok with "LFT Hinv Htok") as "[#Hinv $]". done.
+    iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]". done.
     iMod (bor_sep with "LFT Hb") as "[Hκν _]". done.
     iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
     { iApply bor_fracture; try done. by rewrite Qp_mult_1_r. }
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 1d2f6512..efb27daa 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -38,12 +38,12 @@ Section rwlockwriteguard.
     iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
     iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
     destruct vl as [|[[|l'|]|][]];
-      try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
     iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
     iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
     iMod (bor_sep with "LFT Hb") as "[Hb H]". done.
     iMod (bor_sep with "LFT H") as "[Hαβ _]". done.
-    iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
+    iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
     iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
     (* FIXME: "iApply lft_intersect_mono" only preserves the later on the last
        goal, as does "iApply (lft_intersect_mono with ">")". *)
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index bc97a804..50928962 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -76,13 +76,13 @@ Section rwlockwriteguard_functions.
     iMod (bor_sep with "LFT H") as "[H↦ H]". done.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
     destruct vl as [|[[|l|]|][]];
-      try by iMod (bor_persistent_tok with "LFT H Hα") as "[>[] _]".
+      try by iMod (bor_persistent with "LFT H Hα") as "[>[] _]".
     rewrite heap_mapsto_vec_singleton.
     iMod (bor_exists with "LFT H") as (γ) "H". done.
     iMod (bor_exists with "LFT H") as (δ) "H". done.
     iMod (bor_sep with "LFT H") as "[Hb H]". done.
     iMod (bor_sep with "LFT H") as "[Hβδ _]". done.
-    iMod (bor_persistent_tok with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
+    iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
     iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
     wp_bind (!(LitV lx'))%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
     wp_read. wp_op. wp_let. iMod "Hb".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index f022a478..05fa25c2 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -70,7 +70,7 @@ Section own.
     iMod (bor_exists with "LFT Hshr") as (vl) "Hb"; first solve_ndisj.
     iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first solve_ndisj.
     destruct vl as [|[[|l'|]|][]];
-      try (iMod (bor_persistent_tok with "LFT Hb2 Htok") as "[>[]_]"; solve_ndisj).
+      try (iMod (bor_persistent with "LFT Hb2 Htok") as "[>[]_]"; solve_ndisj).
     iFrame. iExists l'. rewrite heap_mapsto_vec_singleton.
     iMod (bor_sep with "LFT Hb2") as "[Hb2 _]"; first solve_ndisj.
     iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 5d2dd588..34fb8dd9 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -133,7 +133,7 @@ Next Obligation.
   iIntros (?? st E κ l tid ??) "#LFT Hmt Hκ".
   iMod (bor_exists with "LFT Hmt") as (vl) "Hmt"; first solve_ndisj.
   iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]"; first solve_ndisj.
-  iMod (bor_persistent_tok with "LFT Hown Hκ") as "[Hown $]"; first solve_ndisj.
+  iMod (bor_persistent with "LFT Hown Hκ") as "[Hown $]"; first solve_ndisj.
   iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; by eauto with iFrame.
 Qed.
 Next Obligation.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 6d24d83e..ec9013bd 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -25,7 +25,7 @@ Section uniq_bor.
     move=> κ ty N κ' l tid ??/=. iIntros "#LFT Hshr Htok".
     iMod (bor_exists with "LFT Hshr") as ([|[[|l'|]|][]]) "Hb"; first solve_ndisj;
       (iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]"; first solve_ndisj);
-      try (iMod (bor_persistent_tok with "LFT Hb2 Htok") as "[>[] _]"; solve_ndisj).
+      try (iMod (bor_persistent with "LFT Hb2 Htok") as "[>[] _]"; solve_ndisj).
     iFrame. iExists l'. subst. rewrite heap_mapsto_vec_singleton.
     iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$"; first solve_ndisj.
     iApply delay_sharing_nested; try done. iApply lft_incl_refl.
-- 
GitLab