From 9c1d9abdafffbffc438583d181485d2252f530a4 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 4 May 2021 12:02:45 +0200
Subject: [PATCH] The introduction pattern \!# is deprecated. Replace by \!>.
---
theories/lang/heap.v | 2 +-
theories/lang/lib/arc.v | 28 ++++-----
theories/lang/lib/lock.v | 8 +--
theories/lang/lib/spawn.v | 2 +-
theories/lifetime/frac_borrow.v | 2 +-
theories/lifetime/lifetime.v | 6 +-
theories/lifetime/model/creation.v | 12 ++--
theories/lifetime/model/faking.v | 2 +-
theories/lifetime/model/primitive.v | 8 +--
theories/typing/examples/get_x.v | 2 +-
theories/typing/examples/init_prod.v | 2 +-
theories/typing/examples/lazy_lft.v | 2 +-
theories/typing/examples/nonlexical.v | 4 +-
theories/typing/examples/rebor.v | 2 +-
theories/typing/examples/unbox.v | 2 +-
theories/typing/fixpoint.v | 2 +-
theories/typing/function.v | 14 ++---
theories/typing/lft_contexts.v | 26 ++++----
theories/typing/lib/arc.v | 60 +++++++++----------
theories/typing/lib/brandedvec.v | 8 +--
theories/typing/lib/cell.v | 22 +++----
theories/typing/lib/diverging_static.v | 10 ++--
theories/typing/lib/fake_shared.v | 12 ++--
theories/typing/lib/ghostcell.v | 22 +++----
theories/typing/lib/join.v | 2 +-
theories/typing/lib/mutex/mutex.v | 12 ++--
theories/typing/lib/mutex/mutexguard.v | 16 ++---
theories/typing/lib/option.v | 8 +--
theories/typing/lib/panic.v | 2 +-
theories/typing/lib/rc/rc.v | 24 ++++----
theories/typing/lib/rc/weak.v | 16 ++---
theories/typing/lib/refcell/ref.v | 2 +-
theories/typing/lib/refcell/ref_code.v | 10 ++--
theories/typing/lib/refcell/refcell.v | 8 +--
theories/typing/lib/refcell/refcell_code.v | 14 ++---
theories/typing/lib/refcell/refmut.v | 6 +-
theories/typing/lib/refcell/refmut_code.v | 10 ++--
theories/typing/lib/rwlock/rwlock.v | 8 +--
theories/typing/lib/rwlock/rwlock_code.v | 16 ++---
theories/typing/lib/rwlock/rwlockreadguard.v | 4 +-
.../typing/lib/rwlock/rwlockreadguard_code.v | 6 +-
theories/typing/lib/rwlock/rwlockwriteguard.v | 8 +--
.../typing/lib/rwlock/rwlockwriteguard_code.v | 6 +-
theories/typing/lib/spawn.v | 8 +--
theories/typing/lib/swap.v | 2 +-
theories/typing/lib/take_mut.v | 2 +-
theories/typing/own.v | 12 ++--
theories/typing/product.v | 14 ++---
theories/typing/programs.v | 2 +-
theories/typing/shr_bor.v | 6 +-
theories/typing/sum.v | 4 +-
theories/typing/type.v | 30 +++++-----
theories/typing/uninit.v | 2 +-
theories/typing/uniq_bor.v | 10 ++--
theories/typing/util.v | 4 +-
55 files changed, 267 insertions(+), 267 deletions(-)
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 5fa2cf3c..19b0c821 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -205,7 +205,7 @@ Section heap.
Lemma heap_mapsto_pred_iff_proper l q Φ1 Φ2 :
□ (∀ vl, Φ1 vl ↔ Φ2 vl) -∗ □ (l ↦∗{q}: Φ1 ↔ l ↦∗{q}: Φ2).
Proof.
- iIntros "#HΦ !#". iSplit; iIntros; iApply (heap_mapsto_pred_wand with "[-]"); try done; [|];
+ iIntros "#HΦ !>". iSplit; iIntros; iApply (heap_mapsto_pred_wand with "[-]"); try done; [|];
iIntros; by iApply "HΦ".
Qed.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index c648706c..efe5db06 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -222,7 +222,7 @@ Section arc.
is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
{{{ P }}} strong_count [ #l] {{{ (c : nat), RET #c; P ∗ ⌜(c > 0)%nat⌠}}}.
Proof using HP1.
- iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec.
+ iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec.
iInv N as (st) "[>Hâ— H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(?& strong &?&?&[-> _]).
@@ -238,7 +238,7 @@ Section arc.
is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
{{{ P }}} weak_count [ #l] {{{ (c : Z), RET #c; P ∗ ⌜c >= -1⌠}}}.
Proof using HP1.
- iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op.
+ iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_op.
iInv N as (st) "[>Hâ— H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(?& strong &wl&?&[-> _]).
@@ -257,7 +257,7 @@ Section arc.
{{{ P }}} clone_arc [ #l]
{{{ q', RET #☠; P ∗ arc_tok γ q' ∗ P1 q' }}}.
Proof using HP1.
- iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
+ iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
iInv N as (st) "[>Hâ— H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(?& strong &?&?&[-> _]).
@@ -292,7 +292,7 @@ Section arc.
is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
{{{ P }}} downgrade [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}.
Proof.
- iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
+ iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iInv N as (st) "[>Hâ— H]" "Hclose1".
iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(?&?& wlock & weak &[-> _]).
@@ -343,11 +343,11 @@ Section arc.
is_arc P1 P2 N γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗
{{{ P }}} clone_weak [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}.
Proof.
- iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
+ iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iAssert (□ (P ={⊤,⊤∖↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
((l +ₗ 1) ↦ #(w + 1) ={⊤∖↑N,⊤}=∗ P ∗ weak_tok γ) ∧
((l +ₗ 1) ↦ #w ={⊤∖↑N,⊤}=∗ P)))%I as "#Hproto".
- { iIntros "!# HP". iInv N as (st) "[>Hâ— H]" "Hclose1".
+ { iIntros "!> HP". iInv N as (st) "[>Hâ— H]" "Hclose1".
iMod ("Hacc" with "HP") as "[Hown Hclose2]".
iDestruct (weak_tok_auth_val with "Hâ— Hown") as %(st' & weak & -> & Hval).
iMod ("Hclose2" with "Hown") as "HP".
@@ -391,11 +391,11 @@ Section arc.
{{{ P }}} upgrade [ #l]
{{{ (b : bool) q, RET #b; P ∗ if b then arc_tok γ q ∗ P1 q else True }}}.
Proof using HP1.
- iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
+ iIntros "#INV #Hacc !> * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
iAssert (□ (P ={⊤,∅}=∗ ∃ s : Z, l ↦ #s ∗
(⌜s ≠0⌠-∗ l ↦ #(s + 1) ={∅,⊤}=∗ ∃ q, P ∗ arc_tok γ q ∗ ▷ P1 q) ∧
(l ↦ #s ={∅,⊤}=∗ P)))%I as "#Hproto".
- { iIntros "!# HP". iInv N as (st) "[>Hâ— H]" "Hclose1".
+ { iIntros "!> HP". iInv N as (st) "[>Hâ— H]" "Hclose1".
iMod ("Hacc" with "HP") as "[Hown Hclose2]".
iDestruct (weak_tok_auth_val with "Hâ— Hown") as %(st' & weak & -> & Hval).
destruct st' as [[[[??]?]| |]|]; try done; iExists _.
@@ -437,12 +437,12 @@ Section arc.
{{{ weak_tok γ }}} drop_weak [ #l]
{{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0 else True }}}.
Proof.
- iIntros "#INV !# * Hown HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
+ iIntros "#INV !> * Hown HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
iAssert (□ (weak_tok γ ={⊤,⊤ ∖ ↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
((l +ₗ 1) ↦ #(w - 1) ={⊤ ∖ ↑N,⊤}=∗ ⌜w ≠1⌠∨
▷ P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0) ∧
((l +ₗ 1) ↦ #w ={⊤ ∖ ↑N,⊤}=∗ weak_tok γ)))%I as "#Hproto".
- { iIntros "!# Hown". iInv N as (st) "[>Hâ— H]" "Hclose1".
+ { iIntros "!> Hown". iInv N as (st) "[>Hâ— H]" "Hclose1".
iDestruct (weak_tok_auth_val with "Hâ— Hown") as %(st' & weak & -> & Hval).
destruct st' as [[[[??][?|]]| |]|]; try done; [|iExists _..].
- by iDestruct "H" as (?) "(_ & _ & _ & _ & >%)".
@@ -503,7 +503,7 @@ Section arc.
{{{ arc_tok γ q ∗ P1 q }}} drop_arc [ #l]
{{{ (b : bool), RET #b ; if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else True }}}.
Proof using HP1.
- iIntros "#INV !# * [Hown HP1] HΦ". iLöb as "IH".
+ iIntros "#INV !> * [Hown HP1] HΦ". iLöb as "IH".
wp_rec. wp_bind (!ˢᶜ_)%E. iInv N as (st) "[>H◠H]" "Hclose".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(?& s &?&?&[-> _]).
iDestruct "H" as (x') "(? & ? & ? & ?)". wp_read.
@@ -543,7 +543,7 @@ Section arc.
{{{ (b : bool), RET #b ;
if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else arc_tok γ q ∗ P1 q }}}.
Proof using HP1.
- iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. iInv N as (st) "[>H◠H]" "Hclose".
+ iIntros "#INV !> * [Hown HP1] HΦ". wp_rec. iInv N as (st) "[>H◠H]" "Hclose".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(q' & s & wl & w &[-> Hqq']).
iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
destruct (decide (s = xH)) as [->|?].
@@ -566,7 +566,7 @@ Section arc.
if b then l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ P1 1
else arc_tok γ q ∗ P1 q }}}.
Proof using HP1.
- iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _). wp_op.
+ iIntros "#INV !> * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _). wp_op.
iInv N as (st) "[>Hâ— H]" "Hclose".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(? & ? & wl & w &[-> _]).
iDestruct "H" as (?) "(>Hq'' & HP1' & >Hs & >Hw)".
@@ -633,7 +633,7 @@ Section arc.
| _ (* 2 *) => arc_tok γ q ∗ P1 q
end }}}.
Proof using HP1.
- iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _).
+ iIntros "#INV !> * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _).
iInv N as (st) "[>Hâ— H]" "Hclose".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(q' & s & wl & w &[-> Hqq']).
iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 328133ab..ae421b61 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -36,7 +36,7 @@ Section proof.
Lemma lock_proto_iff_proper l R R' :
□ (R ↔ R') -∗ □ (lock_proto l R ↔ lock_proto l R').
Proof.
- iIntros "#HR !#". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck").
+ iIntros "#HR !>". iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck").
- done.
- iModIntro; iSplit; iIntros; by iApply "HR".
Qed.
@@ -77,7 +77,7 @@ Section proof.
{{{ P }}} try_acquire [ #l ] @ E
{{{ b, RET #b; (if b is true then R else True) ∗ P }}}.
Proof.
- iIntros "#Hproto !# * HP HΦ".
+ iIntros "#Hproto !> * HP HΦ".
wp_rec. iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
iDestruct "Hinv" as ([]) "[Hl HR]".
- wp_apply (wp_cas_int_fail with "Hl"); [done..|]. iIntros "Hl".
@@ -92,7 +92,7 @@ Section proof.
□ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
{{{ P }}} acquire [ #l ] @ E {{{ RET #☠; R ∗ P }}}.
Proof.
- iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
+ iIntros "#Hproto !> * HP HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]).
- iIntros "[HR Hown]". wp_if. iApply "HΦ"; iFrame.
- iIntros "[_ Hown]". wp_if. iApply ("IH" with "Hown HΦ").
@@ -102,7 +102,7 @@ Section proof.
□ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
{{{ R ∗ P }}} release [ #l ] @ E {{{ RET #☠; P }}}.
Proof.
- iIntros "#Hproto !# * (HR & HP) HΦ". wp_let.
+ iIntros "#Hproto !> * (HR & HP) HΦ". wp_let.
iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
iDestruct "Hinv" as (b) "[? _]". wp_write. iApply "HΦ".
iApply "Hclose". iExists false. by iFrame.
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 11340bc2..55feed47 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -119,7 +119,7 @@ Lemma join_handle_impl (Ψ1 Ψ2 : val → iProp Σ) c :
□ (∀ v, Ψ1 v -∗ Ψ2 v) -∗ join_handle c Ψ1 -∗ join_handle c Ψ2.
Proof.
iIntros "#HΨ Hhdl". iDestruct "Hhdl" as (γf γj Ψ') "(Hj & H†& #? & #HΨ')".
- iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!# * ?".
+ iExists γf, γj, Ψ'. iFrame "#∗". iIntros "!> * ?".
iApply "HΨ". iApply "HΨ'". done.
Qed.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index d981e6fa..94aa2a3c 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -137,7 +137,7 @@ Section frac_bor.
lft_ctx -∗ &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
Proof.
iIntros (?) "LFT". iApply (frac_bor_acc' with "LFT"). done.
- iIntros "!#*". rewrite fractional. iSplit; auto.
+ iIntros "!>*". rewrite fractional. iSplit; auto.
Qed.
Lemma frac_bor_shorten κ κ' : κ ⊑ κ' -∗ &frac{κ'}φ -∗ &frac{κ}φ.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 7eee4cbc..9053aaac 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -123,7 +123,7 @@ Qed.
Lemma bor_iff_proper κ P P': ▷ □ (P ↔ P') -∗ □ (&{κ}P ↔ &{κ}P').
Proof.
- iIntros "#HP !#". iSplit; iIntros "?"; iApply bor_iff; try done.
+ iIntros "#HP !>". iSplit; iIntros "?"; iApply bor_iff; try done.
iNext. iModIntro. iSplit; iIntros "?"; iApply "HP"; done.
Qed.
@@ -209,7 +209,7 @@ Qed.
Lemma lft_incl_static κ : ⊢ κ ⊑ static.
Proof.
- iApply lft_incl_intro. iIntros "!#". iSplitR.
+ iApply lft_incl_intro. iIntros "!>". iSplitR.
- iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
- iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
Qed.
@@ -228,7 +228,7 @@ Lemma lft_eternalize E q κ :
Proof.
iIntros "Hκ". iMod (inv_alloc lftN _ (∃ q, q.[κ])%I with "[Hκ]") as "#Hnv".
{ iExists _. done. }
- iApply lft_incl_intro. iIntros "!> !#". iSplitL.
+ iApply lft_incl_intro. iIntros "!> !>". iSplitL.
- iIntros (q') "$". iInv lftN as ">Hκ" "Hclose". iDestruct "Hκ" as (q'') "[Hκ1 Hκ2]".
iMod ("Hclose" with "[Hκ2]") as "_". { iExists _. done. }
iModIntro. iExists _. iFrame. iIntros "_". done.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 5000f19b..8d0a45bf 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -130,7 +130,7 @@ Proof.
- iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
iModIntro; iExists Λ.
rewrite {1}/lft_tok big_sepMS_singleton. iSplit; first done. iFrame "HΛ".
- clear I A HΛ. iIntros "!# HΛ".
+ clear I A HΛ. iIntros "!> HΛ".
iApply (step_fupd_mask_mono (↑lftN ∪ ↑lft_userN) _ ((↑lftN ∪ ↑lft_userN)∖↑mgmtN)).
{ (* FIXME solve_ndisj should really handle this... *)
assert (↑lft_userN ## ↑mgmtN) by solve_ndisj.
@@ -153,11 +153,11 @@ Proof.
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 "!#".
+ { iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!>".
iIntros (κ [[Hκ _]%elem_of_filter _]%elem_of_difference) "?".
by iApply lft_inv_alive_in. }
iAssert ([∗ set] κ ∈ K, lft_inv A κ ∗ [†κ])%I with "[HinvK]" as "HinvK".
- { iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
+ { iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!>".
iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
iApply fupd_trans.
iApply (fupd_mask_mono (↑lft_userN ∪ ↑borN ∪ ↑inhN)).
@@ -181,15 +181,15 @@ Proof.
rewrite /own_alft_auth /to_alftUR fmap_insert. iFrame "HA HI".
rewrite HI !big_sepS_union //.
iSplitL "HinvK HinvD"; first iSplitL "HinvK".
- - iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
+ - iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!>".
iIntros (κ [? _]%elem_of_kill_set) "Hdead". rewrite /lft_inv.
iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false'.
- - iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!#".
+ - iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!>".
iIntros (κ [[Hκ HκI]%elem_of_filter HκK]%elem_of_difference) "Halive".
rewrite /lft_inv. iLeft. iFrame "Halive". iPureIntro.
apply lft_alive_in_insert_false; last done.
move: HκK. rewrite elem_of_kill_set -(elem_of_dom (D:=gset lft)). set_solver +HκI.
- - iApply (@big_sepS_impl with "[$Hinv]"); iIntros "!#".
+ - iApply (@big_sepS_impl with "[$Hinv]"); iIntros "!>".
rewrite /lft_inv. iIntros (κ Hκ) "[[? %]|[? %]]".
+ iLeft. iFrame. iPureIntro.
apply lft_alive_in_insert_false; last done. intros ?.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 5636fc4e..101ca0ee 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -63,7 +63,7 @@ Proof.
{ by iDestruct "Hdeadandalive" as "[? _]". }
iPureIntro. exists Λ. rewrite lookup_insert; auto. }
iNext. iApply (@big_sepS_impl with "[$Hinv]").
- rewrite /lft_inv. iIntros "!#"; iIntros (κ' ?%elem_of_dom)
+ rewrite /lft_inv. iIntros "!>"; iIntros (κ' ?%elem_of_dom)
"[[HA HA']|[HA HA']]"; iDestruct "HA'" as %HA.
+ iLeft. iFrame "HA". iPureIntro. by apply lft_alive_in_insert.
+ iRight. iFrame "HA". iPureIntro. by apply lft_dead_in_insert.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index bfe5b0c8..043fb967 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -335,7 +335,7 @@ Proof. reflexivity. Qed.
Lemma lft_intersect_incl_l κ κ' : ⊢ κ ⊓ κ' ⊑ κ.
Proof.
- unfold lft_incl. iIntros "!#". iSplitR.
+ unfold lft_incl. iIntros "!>". iSplitR.
- iIntros (q). rewrite <-lft_tok_sep. iIntros "[H Hf]". iExists q. iFrame.
rewrite <-lft_tok_sep. by iIntros "!>{$Hf}$".
- iIntros "? !>". iApply lft_dead_or. auto.
@@ -345,11 +345,11 @@ Lemma lft_intersect_incl_r κ κ' : ⊢ κ ⊓ κ' ⊑ κ'.
Proof. rewrite comm. apply lft_intersect_incl_l. Qed.
Lemma lft_incl_refl κ : ⊢ κ ⊑ κ.
-Proof. unfold lft_incl. iIntros "!#"; iSplitR; auto 10 with iFrame. Qed.
+Proof. unfold lft_incl. iIntros "!>"; iSplitR; auto 10 with iFrame. Qed.
Lemma lft_incl_trans κ κ' κ'' : κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
Proof.
- rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†] !#". iSplitR.
+ rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†] !>". iSplitR.
- iIntros (q) "Hκ".
iMod ("H1" with "Hκ") as (q') "[Hκ' Hclose]".
iMod ("H2" with "Hκ'") as (q'') "[Hκ'' Hclose']".
@@ -369,7 +369,7 @@ Qed.
Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⊓ κ''.
Proof.
- rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
+ rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!>". iSplitR.
- iIntros (q) "[Hκ'1 Hκ'2]".
iMod ("H1" with "Hκ'1") as (q') "[Hκ' Hclose']".
iMod ("H2" with "Hκ'2") as (q'') "[Hκ'' Hclose'']".
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index e71c3dec..68a0e610 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -14,7 +14,7 @@ Section get_x.
Lemma get_x_type :
typed_val get_x (fn(∀ α, ∅; &uniq{α}(Π[int; int])) → &shr{α}int).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α Ï ret p).
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>". iIntros (α Ï ret p).
inv_vec p=>p. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 49723aed..46cf5855 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -14,7 +14,7 @@ Section init_prod.
Lemma init_prod_type : typed_val init_prod (fn(∅; int, int) → Π[int;int]).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([] Ï ret p). inv_vec p=>x y. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 0bc054bc..0286a518 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -19,7 +19,7 @@ Section lazy_lft.
Lemma lazy_lft_type : typed_val lazy_lft (fn(∅) → unit).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([] Ï ret p). inv_vec p. simpl_subst.
iApply (type_newlft []). iIntros (α).
iApply (type_new_subtype (Î [uninit 1;uninit 1])); [solve_typing..|].
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 7e78bb31..eecd7e71 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -75,7 +75,7 @@ Section non_lexical.
Lemma get_default_type :
typed_val get_default (fn(∀ m, ∅; &uniq{m} hashmap, K) → &uniq{m} V).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (m Ï ret p). inv_vec p=>map key. simpl_subst.
iApply type_let; [iApply get_mut_type|solve_typing|].
iIntros (get_mut'). simpl_subst.
@@ -129,7 +129,7 @@ Section non_lexical.
iApply (type_letalloc_n (&uniq{m}V) (own_ptr _ (&uniq{m}V))); [solve_typing..|].
iIntros (r). simpl_subst.
iApply type_jump; solve_typing. }
- iIntros "!# *". inv_vec args=>r. simpl_subst.
+ iIntros "!> *". inv_vec args=>r. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index e761beeb..bb56fe9c 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -19,7 +19,7 @@ Section rebor.
Lemma rebor_type :
typed_val rebor (fn(∅; Π[int; int], Π[int; int]) → int).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([] Ï ret p). inv_vec p=>t1 t2. simpl_subst.
iApply (type_newlft []). iIntros (α).
iApply (type_letalloc_1 (&uniq{α}(Π[int; int]))); [solve_typing..|]. iIntros (x). simpl_subst.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index b27bbd92..05fa7414 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -14,7 +14,7 @@ Section unbox.
Lemma ubox_type :
typed_val unbox (fn(∀ α, ∅; &uniq{α}(box(Π[int; int]))) → &uniq{α}int).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret b). inv_vec b=>b. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (b'); simpl_subst.
iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 76c9e197..cec43a3b 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -93,7 +93,7 @@ Section fixpoint.
Proof.
unfold eqtype, subtype, type_incl.
setoid_rewrite <-fixpointK_unfold; [| by apply type_contractive_ne, _..].
- split; iIntros (qmax qL) "_ !# _"; (iSplit; first done); iSplit; iIntros "!#*$".
+ split; iIntros (qmax qL) "_ !> _"; (iSplit; first done); iSplit; iIntros "!>*$".
Qed.
End fixpoint.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 534f80e5..53f469b3 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -161,15 +161,15 @@ Section typing.
iDestruct (HE with "HL0") as "#HE".
iDestruct (subtype_Forall2_llctx_noend with "HL0") as "#Htys"; first done.
iDestruct (Hty with "HL0") as "#Hty".
- iClear "∗". iIntros "!# #HEE".
+ iClear "∗". iIntros "!> #HEE".
iSplit; last iSplit.
- by iApply "HE".
- by iApply "Htys".
- by iApply "Hty". }
- iClear "∗". clear Hcons. iIntros "!# #HE0 * Hf".
+ iClear "∗". clear Hcons. iIntros "!> #HE0 * Hf".
iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists fb, kb, xb, e, _. iSplit; first done. iSplit; first done. iNext.
- rewrite /typed_body. iIntros (x Ï k xl) "!# * #LFT #HE' Htl HL HC HT".
+ rewrite /typed_body. iIntros (x Ï k xl) "!> * #LFT #HE' Htl HL HC HT".
iDestruct ("Hcons" with "[$]") as "#(HE & Htys & Hty)".
iApply ("Hf" with "LFT HE Htl HL [HC] [HT]").
- unfold cctx_interp. iIntros (elt) "Helt".
@@ -185,7 +185,7 @@ Section typing.
-{2}(fst_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
-{2}(snd_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
!zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !big_sepL_fmap.
- iApply (big_sepL_impl with "HT"). iIntros "!#".
+ iApply (big_sepL_impl with "HT"). iIntros "!>".
iIntros (i [p [ty1' ty2']]) "#Hzip H /=".
iDestruct "H" as (v) "[? Hown]". iExists v. iFrame.
rewrite !lookup_zip_with.
@@ -229,7 +229,7 @@ Section typing.
subtype E0 L0 (fn (n:=n) fp) (fn (fp ∘ σ)).
Proof.
apply subtype_simple_type=>//= qmax qL.
- iIntros "_ !# _ * Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
+ iIntros "_ !> _ * Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists fb, kb, xb, e, _. iSplit; first done. iSplit; first done.
rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
Qed.
@@ -419,7 +419,7 @@ Section typing.
rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
{ simpl. rewrite decide_left. done. }
iExists fb, _, argsb, e, _. iSplit; first done. iSplit; first done. iNext.
- iIntros (x Ï k args) "!#". iIntros (tid' qmax') "_ HE Htl HL HC HT'".
+ iIntros (x Ï k args) "!>". iIntros (tid' qmax') "_ HE Htl HL HC HT'".
iApply ("Hbody" with "LFT HE Htl HL HC").
rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
by iApply sendc_change_tid.
@@ -438,7 +438,7 @@ Section typing.
(subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
typed_instruction_ty E L T ef (fn fp).
Proof.
- iIntros (??) "#He". iApply type_rec; try done. iIntros "!# *".
+ iIntros (??) "#He". iApply type_rec; try done. iIntros "!> *".
iApply typed_body_mono; last iApply "He"; try done.
eapply contains_tctx_incl. by constructor.
Qed.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 268f972b..265c642b 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -157,7 +157,7 @@ Section lft_contexts.
Lemma lctx_lft_incl_refl κ : lctx_lft_incl κ κ.
Proof.
- iIntros (qmax qL) "_ !# _".
+ iIntros (qmax qL) "_ !> _".
iPureIntro. apply lft_incl_syn_refl.
Qed.
@@ -167,7 +167,7 @@ Section lft_contexts.
iIntros (??? H1 H2 ??) "HL".
iDestruct (H1 with "HL") as "#H1".
iDestruct (H2 with "HL") as "#H2".
- iClear "∗". iIntros "!# #HE".
+ iClear "∗". iIntros "!> #HE".
iDestruct ("H1" with "HE") as "%". iDestruct ("H2" with "HE") as "%".
iPureIntro.
by eapply lft_incl_syn_trans.
@@ -186,7 +186,7 @@ Section lft_contexts.
Qed.
Lemma lctx_lft_incl_static κ : lctx_lft_incl κ static.
- Proof. iIntros (qmax qL) "_ !# _". iPureIntro. apply lft_incl_syn_static. Qed.
+ Proof. iIntros (qmax qL) "_ !> _". iPureIntro. apply lft_incl_syn_static. Qed.
Lemma lctx_lft_incl_local κ κ' κs :
κ ⊑ₗ κs ∈ L → κ' ∈ κs → lctx_lft_incl κ κ'.
@@ -194,7 +194,7 @@ Section lft_contexts.
iIntros (? Hκ'κs qmax qL) "H".
iDestruct (big_sepL_elem_of with "H") as "H"; first done.
iDestruct "H" as (κ'') "[EQ _]". iDestruct "EQ" as %EQ.
- simpl in EQ; subst. iIntros "!# #HE".
+ simpl in EQ; subst. iIntros "!> #HE".
iPureIntro.
eapply lft_incl_syn_trans; first apply lft_intersect_incl_syn_l.
by apply lft_intersect_list_elem_of_incl_syn.
@@ -206,7 +206,7 @@ Section lft_contexts.
Lemma lctx_lft_incl_external κ κ' : κ ⊑ₑ κ' ∈ E → lctx_lft_incl κ κ'.
Proof.
- iIntros (???) "_ !# #HE".
+ iIntros (???) "_ !> #HE".
rewrite /elctx_interp /elctx_elt_interp big_sepL_elem_of //. done.
Qed.
@@ -221,7 +221,7 @@ Section lft_contexts.
iIntros (Hκ' Hκ'' ??) "HL".
iDestruct (Hκ' with "HL") as "#Hκ'".
iDestruct (Hκ'' with "HL") as "#Hκ''".
- iIntros "!# #HE".
+ iIntros "!> #HE".
iDestruct ("Hκ'" with "HE") as "%".
iDestruct ("Hκ''" with "HE") as "%".
iPureIntro.
@@ -234,7 +234,7 @@ Section lft_contexts.
Proof.
iIntros (Hκ' ??) "HL".
iDestruct (Hκ' with "HL") as "#Hκ'".
- iIntros "!# #HE". iDestruct ("Hκ'" with "HE") as "%". iPureIntro.
+ iIntros "!> #HE". iDestruct ("Hκ'" with "HE") as "%". iPureIntro.
eapply lft_incl_syn_trans; last eassumption.
by apply lft_intersect_incl_syn_l.
Qed.
@@ -245,7 +245,7 @@ Section lft_contexts.
Proof.
iIntros (Hκ' ??) "HL".
iDestruct (Hκ' with "HL") as "#Hκ'".
- iIntros "!# #HE". iDestruct ("Hκ'" with "HE") as "%". iPureIntro.
+ iIntros "!> #HE". iDestruct ("Hκ'" with "HE") as "%". iPureIntro.
eapply lft_incl_syn_trans; last eassumption.
by apply lft_intersect_incl_syn_r.
Qed.
@@ -378,7 +378,7 @@ Section lft_contexts.
∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ elctx_interp E').
Lemma elctx_sat_nil : elctx_sat [].
- Proof. iIntros (??) "_ !# _". by rewrite /elctx_interp /=. Qed.
+ Proof. iIntros (??) "_ !> _". by rewrite /elctx_interp /=. Qed.
Lemma elctx_sat_lft_incl E' κ κ' :
lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat ((κ ⊑ₑ κ') :: E').
@@ -386,7 +386,7 @@ Section lft_contexts.
iIntros (Hκκ' HE' qmax qL) "HL".
iDestruct (Hκκ' with "HL") as "#Hincl".
iDestruct (HE' with "HL") as "#HE'".
- iClear "∗". iIntros "!# #HE". iSplit.
+ iClear "∗". iIntros "!> #HE". iSplit.
- by iApply "Hincl".
- by iApply "HE'".
Qed.
@@ -397,13 +397,13 @@ Section lft_contexts.
iIntros (HE1 HE2 ??) "HL".
iDestruct (HE1 with "HL") as "#HE1".
iDestruct (HE2 with "HL") as "#HE2".
- iClear "∗". iIntros "!# #HE".
+ iClear "∗". iIntros "!> #HE".
iDestruct ("HE1" with "HE") as "#$".
iApply ("HE2" with "HE").
Qed.
Lemma elctx_sat_refl : elctx_sat E.
- Proof. iIntros (??) "_ !# ?". done. Qed.
+ Proof. iIntros (??) "_ !> ?". done. Qed.
End lft_contexts.
Arguments lctx_lft_incl {_ _} _ _ _ _.
@@ -417,7 +417,7 @@ Arguments lctx_lft_alive_tok_noend {_ _ _ _ _} _ _ _.
Lemma elctx_sat_submseteq `{!invG Σ, !lftG Σ} E E' L :
E' ⊆+ E → elctx_sat E L E'.
-Proof. iIntros (HE' ??) "_ !# H". by iApply big_sepL_submseteq. Qed.
+Proof. iIntros (HE' ??) "_ !> H". by iApply big_sepL_submseteq. Qed.
Global Hint Resolve
lctx_lft_incl_refl lctx_lft_incl_static lctx_lft_incl_local'
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 88ad58aa..beca6e4f 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -43,7 +43,7 @@ Section arc.
iIntros "#(Heqsz & Hinclo & Hincls) #(?& Hs & Hvs)".
iDestruct "Heqsz" as %->. iFrame "#". iSplit.
- iDestruct "Hs" as "[?|?]"; last auto. iLeft. by iApply "Hincls".
- - iIntros "!# Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
+ - iIntros "!> Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
iMod "H" as "($ & H & $)". iDestruct "H" as (vl) "[??]". iExists _.
iFrame. by iApply "Hinclo".
Qed.
@@ -52,7 +52,7 @@ Section arc.
arc_persist tid ν γ l ty -∗ arc_persist tid' ν γ l ty.
Proof.
iIntros "#($ & ? & Hvs)". rewrite sync_change_tid. iFrame "#".
- iIntros "!# Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
+ iIntros "!> Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
iMod "H" as "($ & H & $)". iDestruct "H" as (vl) "?". iExists _.
by rewrite send_change_tid.
Qed.
@@ -83,7 +83,7 @@ Section arc.
as (γ q') "(#? & ? & ?)".
iExists _, _, _. iFrame "∗#". iCombine "H†" "HPend" as "H".
iMod (inv_alloc arc_endN _ ([†ν] ∨ _)%I with "[H]") as "#INV";
- first by iRight; iApply "H". iIntros "!> !# Hν".
+ first by iRight; iApply "H". iIntros "!> !> Hν".
iMod (inv_acc with "INV") as "[[H†|[$ Hvs]] Hclose]";
[set_solver|iDestruct (lft_tok_dead with "Hν H†") as ">[]"|].
rewrite difference_union_distr_l_L difference_diag_L right_id_L
@@ -126,7 +126,7 @@ Section arc.
set (C := (∃ _ _ _, _ ∗ _ ∗ &at{_,_} _)%I).
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I
with "[Hpbown]") as "#Hinv"; first by iLeft.
- iIntros "!> !# * % Htok".
+ iIntros "!> !> * % Htok".
iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ} _)%I with "[Hbtok]" as "Hb".
@@ -185,7 +185,7 @@ Section arc.
iDestruct "Hvl" as (γ ν q) "(#Hpersist & Htk & Hν)".
iRight. iExists _, _, _. iFrame "#∗". by iApply arc_persist_type_incl.
- iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
- iIntros "{$Hfrac} !# * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
+ iIntros "{$Hfrac} !> * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
iModIntro. iNext. iMod "H" as "[$ H]".
iDestruct "H" as (γ ν q') "(Hlft & Hpersist & Hna)".
iExists _, _, _. iFrame. by iApply arc_persist_type_incl.
@@ -195,7 +195,7 @@ Section arc.
Proper (subtype E L ==> subtype E L) arc.
Proof.
iIntros (ty1 ty2 Hsub ??) "HL". iDestruct (Hsub with "HL") as "#Hsub".
- iIntros "!# #HE". iApply arc_subtype. by iApply "Hsub".
+ iIntros "!> #HE". iApply arc_subtype. by iApply "Hsub".
Qed.
Global Instance arc_proper E L :
Proper (eqtype E L ==> eqtype E L) arc.
@@ -247,7 +247,7 @@ Section arc.
set (C := (∃ _ _, _ ∗ &at{_,_} _)%I).
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I
with "[Hpbown]") as "#Hinv"; first by iLeft.
- iIntros "!> !# * % Htok".
+ iIntros "!> !> * % Htok".
iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ} _)%I with "[Hbtok]" as "Hb".
@@ -295,7 +295,7 @@ Section arc.
iDestruct "Hvl" as (γ ν) "(#Hpersist & Htk)".
iExists _, _. iFrame "#∗". by iApply arc_persist_type_incl.
- iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
- iIntros "{$Hfrac} !# * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
+ iIntros "{$Hfrac} !> * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
iModIntro. iNext. iMod "H" as "[$ H]". iDestruct "H" as (γ ν) "[Hpersist Hna]".
iExists _, _. iFrame. by iApply arc_persist_type_incl.
Qed.
@@ -304,7 +304,7 @@ Section arc.
Proper (subtype E L ==> subtype E L) weak.
Proof.
iIntros (ty1 ty2 Hsub ??) "HL". iDestruct (Hsub with "HL") as "#Hsub".
- iIntros "!# #HE". iApply weak_subtype. by iApply "Hsub".
+ iIntros "!> #HE". iApply weak_subtype. by iApply "Hsub".
Qed.
Global Instance weak_proper E L :
Proper (eqtype E L ==> eqtype E L) weak.
@@ -340,7 +340,7 @@ Section arc.
Lemma arc_new_type ty `{!TyWf ty} :
typed_val (arc_new ty) (fn(∅; ty) → arc ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (rc); simpl_subst.
@@ -382,7 +382,7 @@ Section arc.
Lemma weak_new_type ty `{!TyWf ty} :
typed_val (weak_new ty) (fn(∅) → weak ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg. simpl_subst.
iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (rc); simpl_subst.
@@ -407,7 +407,7 @@ Section arc.
with "Hrcbox↦0 Hrcbox↦1 [-]") as (γ) "[Ha Htok]".
{ rewrite freeable_sz_full_S. iFrame. iExists _. iFrame.
by rewrite vec_to_list_length. }
- iExists γ, ν. iFrame. iSplitL; first by auto. iIntros "!>!>!# Hν".
+ iExists γ, ν. iFrame. iSplitL; first by auto. iIntros "!>!>!> Hν".
iDestruct (lft_tok_dead with "Hν H†") as "[]". }
iApply type_jump; solve_typing.
Qed.
@@ -423,7 +423,7 @@ Section arc.
Lemma arc_deref_type ty `{!TyWf ty} :
typed_val arc_deref (fn(∀ α, ∅; &shr{α}(arc ty)) → &shr{α}ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (x); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -467,7 +467,7 @@ Section arc.
Lemma arc_strong_count_type ty `{!TyWf ty} :
typed_val arc_strong_count (fn(∀ α, ∅; &shr{α}(arc ty)) → int).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -484,7 +484,7 @@ Section arc.
iDestruct "Hproto" as (γ ν q') "#(Hαν & Hpersist & Hrctokb)". iModIntro. wp_let.
wp_apply (strong_count_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
- { iIntros "!# Hα".
+ { iIntros "!> Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
@@ -510,7 +510,7 @@ Section arc.
Lemma arc_weak_count_type ty `{!TyWf ty} :
typed_val arc_weak_count (fn(∀ α, ∅; &shr{α}(arc ty)) → int).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -527,7 +527,7 @@ Section arc.
iDestruct "Hproto" as (γ ν q') "#(Hαν & Hpersist & Hrctokb)". iModIntro. wp_let.
wp_apply (weak_count_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
- { iIntros "!# Hα".
+ { iIntros "!> Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
@@ -555,7 +555,7 @@ Section arc.
Lemma arc_clone_type ty `{!TyWf ty} :
typed_val arc_clone (fn(∀ α, ∅; &shr{α}(arc ty)) → arc ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -572,7 +572,7 @@ Section arc.
iDestruct "Hproto" as (γ ν q') "#(Hαν & Hpersist & Hrctokb)". iModIntro. wp_let.
wp_apply (clone_arc_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
- { iIntros "!# Hα".
+ { iIntros "!> Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
@@ -599,7 +599,7 @@ Section arc.
Lemma weak_clone_type ty `{!TyWf ty} :
typed_val weak_clone (fn(∀ α, ∅; &shr{α}(weak ty)) → weak ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -616,7 +616,7 @@ Section arc.
iDestruct "Hproto" as (γ ν) "#[Hpersist Hrctokb]". iModIntro. wp_let.
wp_apply (clone_weak_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
- { iIntros "!# Hα".
+ { iIntros "!> Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
@@ -643,7 +643,7 @@ Section arc.
Lemma downgrade_type ty `{!TyWf ty} :
typed_val downgrade (fn(∀ α, ∅; &shr{α}(arc ty)) → weak ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -660,7 +660,7 @@ Section arc.
iDestruct "Hproto" as (γ ν q') "#(Hαν & Hpersist & Hrctokb)". iModIntro. wp_let.
wp_apply (downgrade_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
- { iIntros "!# Hα".
+ { iIntros "!> Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
@@ -690,7 +690,7 @@ Section arc.
Lemma upgrade_type ty `{!TyWf ty} :
typed_val upgrade (fn(∀ α, ∅; &shr{α}(weak ty)) → option (arc ty)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -707,7 +707,7 @@ Section arc.
iDestruct "Hproto" as (γ ν) "#[Hpersist Hrctokb]". iModIntro. wp_let.
wp_apply (upgrade_spec (P1 ν) (P2 l' ty.(ty_size)) _ _ _ (q.[α])%I
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
- { iIntros "!# Hα".
+ { iIntros "!> Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
@@ -748,7 +748,7 @@ Section arc.
Lemma arc_drop_type ty `{!TyWf ty} :
typed_val (arc_drop ty) (fn(∅; arc ty) → option ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new (option ty).(ty_size)); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -811,7 +811,7 @@ Section arc.
Lemma weak_drop_type ty `{!TyWf ty} :
typed_val (weak_drop ty) (fn(∅; weak ty) → unit).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new 0); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -854,7 +854,7 @@ Section arc.
Lemma arc_try_unwrap_type ty `{!TyWf ty} :
typed_val (arc_try_unwrap ty) (fn(∅; arc ty) → Σ[ ty; arc ty ]).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new (Σ[ ty; arc ty ]).(ty_size));
[solve_typing..|]; iIntros (r); simpl_subst.
@@ -928,7 +928,7 @@ Section arc.
Lemma arc_get_mut_type ty `{!TyWf ty} :
typed_val arc_get_mut (fn(∀ α, ∅; &uniq{α}(arc ty)) → option (&uniq{α}ty)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -1017,7 +1017,7 @@ Section arc.
typed_val (arc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α}(arc ty)) → &uniq{α} ty).
Proof.
intros Hclone E L. iApply type_fn; [solve_typing..|]. rewrite [(2 + ty_size ty)%nat]lock.
- iIntros "/= !#". iIntros (α Ï ret arg). inv_vec arg=>rcx. simpl_subst.
+ iIntros "/= !>". iIntros (α Ï ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 95685ec3..4779c28b 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -175,7 +175,7 @@ Section typing.
typed_val call_once (fn(∀ α, ∅; F, brandvec α) → R_F) →
typed_val (brandvec_new call_once R_F) (fn(∅; F) → R_F).
Proof.
- iIntros (Hf E L). iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (Hf E L). iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret args). inv_vec args=> env. simpl_subst.
iApply type_let; [apply Hf|solve_typing|]. iIntros (f); simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL Hc (Hf & Henv & _)".
@@ -249,7 +249,7 @@ Section typing.
Lemma brandvec_get_index_type :
typed_val brandvec_get_index (fn(∀ '(α, β), ∅; &shr{β} (brandvec α), int) → option (brandidx α))%T.
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret args). inv_vec args=>v i. simpl_subst.
iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (v'); simpl_subst.
@@ -322,7 +322,7 @@ Section typing.
Lemma brandidx_get_type :
typed_val brandidx_get (fn(∀ '(α, β), ∅; &shr{β} (brandvec α), &shr{β} (brandidx α)) → unit)%T.
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret args). inv_vec args=> s c. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (n); simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (m); simpl_subst.
@@ -372,7 +372,7 @@ Section typing.
Lemma brandvec_push_type :
typed_val brandvec_push (fn(∀ '(α, β), ∅; &uniq{β} (brandvec α)) → brandidx α).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret args). inv_vec args=>(*n *)s. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (n); simpl_subst.
iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index b0e90f84..dd05fb91 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -35,9 +35,9 @@ Section cell.
Global Instance cell_mono E L : Proper (eqtype E L ==> subtype E L) cell.
Proof.
move=>?? /eqtype_unfold EQ. iIntros (??) "HL".
- iDestruct (EQ with "HL") as "#EQ". iIntros "!# #HE".
+ iDestruct (EQ with "HL") as "#EQ". iIntros "!> #HE".
iDestruct ("EQ" with "HE") as "(% & #Hown & #Hshr)".
- iSplit; [done|iSplit; iIntros "!# * H"].
+ iSplit; [done|iSplit; iIntros "!> * H"].
- iApply ("Hown" with "H").
- iApply na_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H";
iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Hown".
@@ -88,7 +88,7 @@ Section typing.
Lemma cell_new_type ty `{!TyWf ty} : typed_val cell_new (fn(∅; ty) → cell ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_jump; [solve_typing..|].
iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
@@ -100,7 +100,7 @@ Section typing.
Lemma cell_into_inner_type ty `{!TyWf ty} :
typed_val cell_into_inner (fn(∅; cell ty) → ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_jump; [solve_typing..|].
iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
@@ -112,7 +112,7 @@ Section typing.
Lemma cell_get_mut_type ty `{!TyWf ty} :
typed_val cell_get_mut (fn(∀ α, ∅; &uniq{α} (cell ty)) → &uniq{α} ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_jump; [solve_typing..|].
iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
@@ -124,7 +124,7 @@ Section typing.
Lemma cell_from_mut_type ty `{!TyWf ty} :
typed_val cell_from_mut (fn(∀ α, ∅; &uniq{α} ty) → &uniq{α} (cell ty)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_jump; [solve_typing..|].
iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
@@ -136,7 +136,7 @@ Section typing.
Lemma cell_into_box_type ty `{!TyWf ty} :
typed_val cell_into_box (fn(∅;box (cell ty)) → box ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_jump; [solve_typing..|].
iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
@@ -148,7 +148,7 @@ Section typing.
Lemma cell_from_box_type ty `{!TyWf ty} :
typed_val cell_from_box (fn(∅; box ty) → box (cell ty)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_jump; [solve_typing..|].
iIntros (???) "#LFT _ $ Hty". rewrite !tctx_interp_singleton /=. done.
@@ -164,7 +164,7 @@ Section typing.
Lemma cell_get_type ty `{!TyWf ty} `(!Copy ty) :
typed_val (cell_get ty) (fn(∀ α, ∅; &shr{α} (cell ty)) → ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
iApply type_letalloc_n; [solve_typing| |iIntros (r); simpl_subst].
@@ -186,7 +186,7 @@ Section typing.
Lemma cell_replace_type ty `{!TyWf ty} :
typed_val (cell_replace ty) (fn(∀ α, ∅; &shr{α}(cell ty), ty) → ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>c x. simpl_subst.
iApply type_deref; [solve_typing..|].
iIntros (c'); simpl_subst.
@@ -239,7 +239,7 @@ Section typing.
Lemma fake_shared_cell_type ty `{!TyWf ty} :
typed_val fake_shared_cell (fn(∀ α, ∅; &uniq{α} ty) → &shr{α}(cell ty)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
rewrite tctx_interp_singleton tctx_hasty_val.
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index 93bebbe2..8d0768aa 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -24,7 +24,7 @@ Section diverging_static.
typed_val (diverging_static_loop call_once)
(fn(∀ α, λ Ï, ty_outlives_E T static; &shr{α} T, F) → ∅).
Proof.
- intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x f. simpl_subst.
iApply type_let; [apply Hf|solve_typing|]. iIntros (call); simpl_subst.
(* Drop to Iris *)
@@ -51,7 +51,7 @@ Section diverging_static.
{ rewrite /llctx_interp /=. done. }
iApply (type_cont [] [] (λ _, [])).
+ iIntros (?). simpl_subst. iApply type_jump; solve_typing.
- + iIntros "!#" (? args). inv_vec args. simpl_subst. iApply type_jump; solve_typing.
+ + iIntros "!>" (? args). inv_vec args. simpl_subst. iApply type_jump; solve_typing.
Qed.
@@ -82,17 +82,17 @@ Section diverging_static.
(fn(∀ α, ∅; T α, F) → ∅).
Proof.
intros type_equivalize_lft_static_bad HWf HTsz HTsub Hf E L.
- iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x f. simpl_subst.
iApply type_let; [apply Hf|solve_typing|]. iIntros (call); simpl_subst.
iApply (type_cont [_] [] (λ r, [(r!!!0%fin:val) ◠box (unit)])).
{ iIntros (k). simpl_subst.
iApply type_equivalize_lft_static_bad.
iApply (type_call [Ï] ()); solve_typing. }
- iIntros "!# *". inv_vec args=>r. simpl_subst.
+ iIntros "!> *". inv_vec args=>r. simpl_subst.
iApply (type_cont [] [] (λ r, [])).
{ iIntros (kloop). simpl_subst. iApply type_jump; solve_typing. }
- iIntros "!# *". inv_vec args. simpl_subst.
+ iIntros "!> *". inv_vec args. simpl_subst.
iApply type_jump; solve_typing.
Qed.
End diverging_static.
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index 9d6b7152..1cd11306 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -12,7 +12,7 @@ Section fake_shared.
typed_val fake_shared_box
(fn(∀ '(α, β), ∅; &shr{α}(&shr{β} ty)) → &shr{α}(box ty)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
rewrite tctx_interp_singleton tctx_hasty_val.
@@ -22,9 +22,9 @@ Section fake_shared.
iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
- { iApply frac_bor_iff; last done. iIntros "!>!# *".
+ { iApply frac_bor_iff; last done. iIntros "!>!> *".
rewrite heap_mapsto_vec_singleton. iSplit; auto. }
- iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
+ iDestruct "H" as "#H". iIntros "!> * % $". iApply step_fupd_intro. set_solver.
simpl. iApply ty_shr_mono; last done.
by iApply lft_incl_syn_sem. }
do 2 wp_seq.
@@ -42,7 +42,7 @@ Section fake_shared.
typed_val fake_shared_box
(fn(∀ '(α, β), ∅; &shr{α}(&shr{β} ty)) → &shr{α}(&uniq{β} ty)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
rewrite tctx_interp_singleton tctx_hasty_val.
@@ -53,9 +53,9 @@ Section fake_shared.
iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
iExists _. iFrame. iDestruct "H" as (vl) "[#Hf H]".
iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
- { iApply frac_bor_iff; last done. iIntros "!>!# *".
+ { iApply frac_bor_iff; last done. iIntros "!>!> *".
rewrite heap_mapsto_vec_singleton. iSplit; auto. }
- iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
+ iDestruct "H" as "#H". iIntros "!> * % $". iApply step_fupd_intro. set_solver.
simpl. iApply ty_shr_mono; last done.
by iApply lft_intersect_incl_l.
}
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index 778e0c3d..8bf2ae43 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -123,10 +123,10 @@ Section ghostcell.
iIntros (α1 α2 [EQ1 EQ2] qmax qL) "HL".
iDestruct (EQ1 with "HL") as "#EQ1'".
iDestruct (EQ2 with "HL") as "#EQ2'".
- iIntros "!# #HE".
+ iIntros "!> #HE".
iDestruct ("EQ1'" with "HE") as %EQ1'.
iDestruct ("EQ2'" with "HE") as %EQ2'.
- iSplit; [|iSplit; iIntros "!# * H"]; simpl.
+ iSplit; [|iSplit; iIntros "!> * H"]; simpl.
- iPureIntro; congruence.
- solve_proper_prepare.
iDestruct "H" as "[$ H]".
@@ -201,13 +201,13 @@ Section ghostcell.
iDestruct (Hty with "HL") as "#Hty".
iDestruct (Hlft1 with "HL") as "#Hlft1".
iDestruct (Hlft2 with "HL") as "#Hlft2".
- iIntros (tid l β) "!# #HE H".
+ iIntros (tid l β) "!> #HE H".
iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
iDestruct ("Hlft1" with "HE") as %Hκ1.
iDestruct ("Hlft2" with "HE") as %Hκ2.
iAssert (□ (&{β}(l ↦∗: ty_own ty1 tid) -∗
&{β}(l ↦∗: ty_own ty2 tid)))%I as "#Hb".
- { iIntros "!# H". iApply bor_iff; last done.
+ { iIntros "!> H". iApply bor_iff; last done.
iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
iFrame; by iApply "Hown". }
iDestruct "H" as (rw) "H"; iExists rw; destruct rw as [rw|]; iFrame "∗";
@@ -303,8 +303,8 @@ Section ghostcell.
iDestruct (EQ'2 with "HL") as "#EQ'".
iDestruct (ghostcell_inv_proper _ _ κ κ' with "HL") as "#Hty1ty2"; [done|done|].
iDestruct (ghostcell_inv_proper _ _ κ' κ with "HL") as "#Hty2ty1"; [done|by symmetry|].
- iIntros "!# #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
- iSplit; [|iSplit; iIntros "!# * H"]; simpl.
+ iIntros "!> #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
+ iSplit; [|iSplit; iIntros "!> * H"]; simpl.
- iPureIntro; congruence.
- by iApply "Hown".
- iDestruct "H" as (a) "H".
@@ -363,7 +363,7 @@ Section ghostcell.
typed_val call_once (fn(∀ α, ∅; F, ghosttoken α) → R_F) →
typed_val (ghosttoken_new call_once R_F) (fn(∅; F) → R_F).
Proof.
- iIntros (Hf E L). iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ iIntros (Hf E L). iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret args). inv_vec args=>env. simpl_subst.
iApply type_let; [apply Hf|solve_typing|]. iIntros (f); simpl_subst.
iApply type_new_subtype; [solve_typing..|].
@@ -412,7 +412,7 @@ Section ghostcell.
Lemma ghostcell_new_type `{!TyWf ty} :
typed_val ghostcell_new (fn(∀ α, ∅; ty) → (ghostcell α ty))%T.
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret args). inv_vec args=>n. simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL Hk Hn".
rewrite tctx_interp_singleton tctx_hasty_val.
@@ -467,7 +467,7 @@ Section ghostcell.
(fn(∀ '(α, β), ∅; &shr{β} (ghostcell α ty), &shr{β} (ghosttoken α)) →
&shr{β} ty)%T.
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret args). inv_vec args=>c s. simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL HC (Hc & Hs & _)".
rewrite !tctx_hasty_val.
@@ -593,7 +593,7 @@ Section ghostcell.
(fn(∀ '(α, β), ∅; &shr{β} (ghostcell α ty), &uniq{β} (ghosttoken α)) →
&uniq{β} ty)%T.
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret args). inv_vec args=>c s. simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL HC (Hc & Hs & _)".
rewrite !tctx_hasty_val.
@@ -693,7 +693,7 @@ Section ghostcell.
typed_val ghostcell_as_mut (fn(∀ '(α, β), ∅; &uniq{β} (ghostcell α ty)) →
&uniq{β} ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret args). inv_vec args=>c. simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL Hk Hc".
rewrite tctx_interp_singleton tctx_hasty_val.
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index d73ae6d5..1bb02860 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -38,7 +38,7 @@ Section join.
typed_val call_once_B (fn(∅; B) → R_B) →
typed_val (join call_once_A call_once_B R_A R_B) (fn(∅; A, B) → Π[R_A; R_B]).
Proof using Type*.
- intros HfA HfB E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros HfA HfB E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>envA envB. simpl_subst.
iApply type_let; [apply HfA|solve_typing|]. iIntros (fA); simpl_subst.
iApply type_let; [apply HfB|solve_typing|]. iIntros (fB); simpl_subst.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 70b5b362..ccd41e0f 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -90,13 +90,13 @@ Section mutex.
Global Instance mutex_mono E L : Proper (eqtype E L ==> subtype E L) mutex.
Proof.
move=>ty1 ty2 /eqtype_unfold EQ. iIntros (??) "HL".
- iDestruct (EQ with "HL") as "#EQ". iIntros "!# #HE". clear EQ.
+ iDestruct (EQ with "HL") as "#EQ". iIntros "!> #HE". clear EQ.
iDestruct ("EQ" with "HE") as "(% & #Howni & _) {EQ}".
iSplit; last iSplit.
- simpl. iPureIntro. f_equiv. done.
- - iIntros "!# * Hvl". destruct vl as [|[[| |n]|]vl]; try done.
+ - iIntros "!> * Hvl". destruct vl as [|[[| |n]|]vl]; try done.
simpl. iDestruct "Hvl" as "[$ Hvl]". by iApply "Howni".
- - iIntros "!# * Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
+ - iIntros "!> * Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
iExists _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
iApply heap_mapsto_pred_iff_proper.
@@ -138,7 +138,7 @@ Section code.
Lemma mutex_new_type ty `{!TyWf ty} :
typed_val (mutex_new ty) (fn(∅; ty) → mutex ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
(* FIXME: It should be possible to infer the `S ty.(ty_size)` here.
This should be done in the @eq external hints added in lft_contexts.v. *)
@@ -177,7 +177,7 @@ Section code.
Lemma mutex_into_inner_type ty `{!TyWf ty} :
typed_val (mutex_into_inner ty) (fn(∅; mutex ty) → ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>m. simpl_subst.
iApply (type_new ty.(ty_size)); [solve_typing..|]; iIntros (x); simpl_subst.
(* Switch to Iris. *)
@@ -216,7 +216,7 @@ Section code.
Lemma mutex_get_mut_type ty `{!TyWf ty} :
typed_val mutex_get_mut (fn(∀ α, ∅; &uniq{α}(mutex ty)) → &uniq{α} ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg); inv_vec arg=>m; simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (m'); simpl_subst.
(* Go to Iris *)
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index d57fac59..dd7ed656 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -64,7 +64,7 @@ Section mguard.
iIntros (??????) "#? H". iDestruct "H" as (l') "[#Hf #H]".
iExists _. iSplit.
- by iApply frac_bor_shorten.
- - iIntros "!# * % Htok".
+ - iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
{ iApply lft_intersect_mono. iApply lft_incl_refl. done. }
iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
@@ -90,7 +90,7 @@ Section mguard.
intros α1 α2 Hα ty1 ty2 Hty. generalize Hty. rewrite eqtype_unfold.
iIntros (Hty' qmax qL) "HL".
iDestruct (Hty' with "HL") as "#Hty". clear Hty'. iDestruct (Hα with "HL") as "#Hα".
- iIntros "!# #HE". iDestruct ("Hα" with "HE") as %Hα12.
+ iIntros "!> #HE". iDestruct ("Hα" with "HE") as %Hα12.
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs) {HE Hty}". iSplit; [done|iSplit; iModIntro].
- iIntros (tid [|[[]|][]]) "H"; try done. simpl.
iDestruct "H" as (β) "(#H⊑ & #Hinv & Hown)".
@@ -105,7 +105,7 @@ Section mguard.
iApply heap_mapsto_pred_iff_proper.
iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
- iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
- iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
+ iDestruct "H" as "[$ #H]". iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
{ iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl. }
iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
@@ -152,7 +152,7 @@ Section code.
□ ((q).[α] ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ (q).[α])).
Proof.
(* FIXME: This should work: iIntros (?? R). *) intros ?? R.
- iIntros "#LFT #Hshr #Hlincl !# Htok".
+ iIntros "#LFT #Hshr #Hlincl !> Htok".
iMod (at_bor_acc_tok with "LFT Hshr Htok") as "[Hproto Hclose1]"; [done..|].
iMod (fupd_mask_subseteq) as "Hclose2"; last iModIntro; first solve_ndisj.
iFrame. iIntros "Hproto". iMod "Hclose2" as "_".
@@ -170,7 +170,7 @@ Section code.
Lemma mutex_lock_type ty `{!TyWf ty} :
typed_val mutex_lock (fn(∀ α, ∅; &shr{α}(mutex ty)) → mutexguard α ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (m); simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (g); simpl_subst.
@@ -207,7 +207,7 @@ Section code.
typed_val mutexguard_derefmut
(fn(∀ '(α, β), ∅; &uniq{α}(mutexguard β ty)) → &uniq{α}ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret arg). inv_vec arg=>g. simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (g'); simpl_subst.
(* Switch to Iris. *)
@@ -249,7 +249,7 @@ Section code.
typed_val mutexguard_derefmut
(fn(∀ '(α, β), ∅; &shr{α}(mutexguard β ty)) → &shr{α}ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret arg). inv_vec arg=>g. simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (g'); simpl_subst.
(* Switch to Iris. *)
@@ -292,7 +292,7 @@ Section code.
Lemma mutexguard_drop_type ty `{!TyWf ty} :
typed_val mutexguard_drop (fn(∀ α, ∅; mutexguard α ty) → unit).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>g. simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (m); simpl_subst.
(* Switch to Iris. *)
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 5ced33ac..15028885 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -32,7 +32,7 @@ Section option.
typed_val
option_as_mut (fn(∀ α, ∅; &uniq{α} (option τ)) → option (&uniq{α}τ)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret p). inv_vec p=>o. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (o'). simpl_subst.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
@@ -44,7 +44,7 @@ Section option.
iApply type_jump; solve_typing.
+ iApply (type_sum_assign (option $ &uniq{α}τ)%T); [try solve_typing..|].
iApply type_jump; solve_typing.
- - iIntros "/= !#". iIntros (k args). inv_vec args. simpl_subst.
+ - iIntros "/= !>". iIntros (k args). inv_vec args. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -62,7 +62,7 @@ Section option.
Lemma option_unwrap_or_type Ï„ `{!TyWf Ï„} :
typed_val (option_unwrap_or τ) (fn(∅; option τ, τ) → τ).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([] Ï ret p). inv_vec p=>o def. simpl_subst.
iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
+ right. iApply type_delete; [solve_typing..|].
@@ -87,7 +87,7 @@ Section option.
Lemma option_unwrap_type Ï„ `{!TyWf Ï„} :
typed_val (option_unwrap τ) (fn(∅; option τ) → τ).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([] Ï ret p). inv_vec p=>o. simpl_subst.
iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
+ right. iApply type_let; [iApply panic_type|solve_typing|].
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 7190f6cc..58a6b02e 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -18,7 +18,7 @@ Section panic.
Lemma panic_type : typed_val panic (fn(∅) → ∅).
Proof.
- intros E L. iApply type_fn; [done|]. iIntros "!# *".
+ intros E L. iApply type_fn; [done|]. iIntros "!> *".
inv_vec args. iIntros (tid qmax) "LFT HE Hna HL Hk HT /=". simpl_subst.
by iApply wp_value.
Qed.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 6f0494ed..d8297185 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -140,7 +140,7 @@ Section rc.
set (C := (∃ _ _ _, _ ∗ _ ∗ &na{_,_,_} _)%I).
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I
with "[Hpbown]") as "#Hinv"; first by iLeft.
- iIntros "!> !# * % Htok".
+ iIntros "!> !> * % Htok".
iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ} _)%I with "[Hbtok]" as "Hb".
@@ -218,7 +218,7 @@ Section rc.
iDestruct "Hvl" as (γ ν q) "(#Hpersist & Htk & Hν)".
iRight. iExists _, _, _. iFrame "#∗". by iApply rc_persist_type_incl.
- iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
- iIntros "{$Hfrac} !# * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
+ iIntros "{$Hfrac} !> * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
iModIntro. iNext. iMod "H" as "[$ H]".
iDestruct "H" as (γ ν q') "(Hlft & Hpersist & Hna)".
iExists _, _, _. iFrame. by iApply rc_persist_type_incl.
@@ -228,7 +228,7 @@ Section rc.
Proper (subtype E L ==> subtype E L) rc.
Proof.
iIntros (ty1 ty2 Hsub ??) "HL". iDestruct (Hsub with "HL") as "#Hsub".
- iIntros "!# #HE". iApply rc_subtype. by iApply "Hsub".
+ iIntros "!> #HE". iApply rc_subtype. by iApply "Hsub".
Qed.
Global Instance rc_proper E L :
Proper (eqtype E L ==> eqtype E L) rc.
@@ -394,7 +394,7 @@ Section code.
Lemma rc_strong_count_type ty `{!TyWf ty} :
typed_val rc_strong_count (fn(∀ α, ∅; &shr{α}(rc ty)) → int).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -453,7 +453,7 @@ Section code.
Lemma rc_weak_count_type ty `{!TyWf ty} :
typed_val rc_weak_count (fn(∀ α, ∅; &shr{α}(rc ty)) → int).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -513,7 +513,7 @@ Section code.
Lemma rc_new_type ty `{!TyWf ty} :
typed_val (rc_new ty) (fn(∅; ty) → rc ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (rc); simpl_subst.
@@ -556,7 +556,7 @@ Section code.
Lemma rc_clone_type ty `{!TyWf ty} :
typed_val rc_clone (fn(∀ α, ∅; &shr{α}(rc ty)) → rc ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -618,7 +618,7 @@ Section code.
Lemma rc_deref_type ty `{!TyWf ty} :
typed_val rc_deref (fn(∀ α, ∅; &shr{α}(rc ty)) → &shr{α}ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (x); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -681,7 +681,7 @@ Section code.
typed_val (rc_try_unwrap ty) (fn(∅; rc ty) → Σ[ ty; rc ty ]).
Proof.
(* TODO: There is a *lot* of duplication between this proof and the one for drop. *)
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new (Σ[ ty; rc ty ]).(ty_size)); [solve_typing..|]; iIntros (r); simpl_subst.
iApply (type_cont [] [Ï âŠ‘â‚— []]
@@ -776,7 +776,7 @@ Section code.
Lemma rc_drop_type ty `{!TyWf ty} :
typed_val (rc_drop ty) (fn(∅; rc ty) → option ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new (option ty).(ty_size)); [solve_typing..|]; iIntros (r); simpl_subst.
iApply (type_cont [] [Ï âŠ‘â‚— []]
@@ -866,7 +866,7 @@ Section code.
Lemma rc_get_mut_type ty `{!TyWf ty} :
typed_val rc_get_mut (fn(∀ α, ∅; &uniq{α}(rc ty)) → option (&uniq{α}ty)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
iApply (type_cont [] [Ï âŠ‘â‚— []]
@@ -999,7 +999,7 @@ Section code.
Proof.
intros Hclone E L. iApply type_fn; [solve_typing..|].
rewrite [(2 + ty_size ty)%nat]lock.
- iIntros "/= !#". iIntros (α Ï ret arg). inv_vec arg=>rcx. simpl_subst.
+ iIntros "/= !>". iIntros (α Ï ret arg). inv_vec arg=>rcx. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply (type_cont [] [Ï âŠ‘â‚— []]
(λ _, [rcx ◠box (uninit 1); r ◠box (&uniq{α}ty)]));
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 83042cbf..5bfb08ea 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -38,7 +38,7 @@ Section weak.
set (C := (∃ _ _, _ ∗ &na{_,_,_} _)%I).
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I with "[Hpbown]") as "#Hinv";
first by iLeft.
- iIntros "!> !# * % Htok".
+ iIntros "!> !> * % Htok".
iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ} _)%I with "[Hbtok]" as "Hb".
@@ -86,7 +86,7 @@ Section weak.
iDestruct "Hvl" as (γ ν) "(#Hpersist & Htok)".
iExists _, _. iFrame "Htok". by iApply rc_persist_type_incl.
- iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
- iIntros "{$Hfrac} !# * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
+ iIntros "{$Hfrac} !> * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
iModIntro. iNext. iMod "H" as "[$ H]". iDestruct "H" as (γ ν) "(Hpersist & Hshr)".
iExists _, _. iFrame "Hshr". by iApply rc_persist_type_incl.
Qed.
@@ -95,7 +95,7 @@ Section weak.
Proper (subtype E L ==> subtype E L) weak.
Proof.
iIntros (ty1 ty2 Hsub ??) "HL". iDestruct (Hsub with "HL") as "#Hsub".
- iIntros "!# #HE". iApply weak_subtype. iApply "Hsub"; done.
+ iIntros "!> #HE". iApply weak_subtype. iApply "Hsub"; done.
Qed.
Global Instance weak_proper E L :
Proper (eqtype E L ==> eqtype E L) weak.
@@ -125,7 +125,7 @@ Section code.
Lemma rc_upgrade_type ty `{!TyWf ty} :
typed_val rc_upgrade (fn(∀ α, ∅; &shr{α}(weak ty)) → option (rc ty)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>w. simpl_subst.
iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
iApply (type_cont [] [Ï âŠ‘â‚— []]
@@ -234,7 +234,7 @@ Section code.
typed_val rc_downgrade (fn(∀ α, ∅; &shr{α}(rc ty)) → weak ty).
Proof.
(* TODO : this is almost identical to rc_clone *)
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -297,7 +297,7 @@ Section code.
typed_val weak_clone (fn(∀ α, ∅; &shr{α}(weak ty)) → weak ty).
Proof.
(* TODO : this is almost identical to rc_clone *)
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
@@ -373,7 +373,7 @@ Section code.
Lemma weak_drop_type ty `{!TyWf ty} :
typed_val (weak_drop ty) (fn(∅; weak ty) → unit).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>w. simpl_subst.
iApply (type_cont [] [Ï âŠ‘â‚— []] (λ _, [w â— box (uninit 1)]));
[solve_typing..| |]; last first.
@@ -448,7 +448,7 @@ Section code.
Lemma weak_new_type ty `{!TyWf ty} :
typed_val (weak_new ty) (fn(∅) → weak ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg. simpl_subst.
iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
iApply (type_new 1); [solve_typing..|]; iIntros (w); simpl_subst.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index ccbcbb47..e146334c 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -82,7 +82,7 @@ Section ref.
Proof.
iIntros (α1 α2 Hα ty1 ty2 Hty qmax qL) "HL".
iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
- iIntros "!# #HE". iDestruct ("Hα" with "HE") as %Hα1α2.
+ iIntros "!> #HE". iDestruct ("Hα" with "HE") as %Hα1α2.
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
- done.
- iIntros (tid [|[[]|][|[[]|][]]]) "H"=>//=.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index f279e518..dec7138d 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -48,7 +48,7 @@ Section ref_functions.
typed_val ref_clone (fn(∀ '(α, β), ∅; &shr{α}(ref β ty)) → ref β ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x').
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -108,7 +108,7 @@ Section ref_functions.
typed_val ref_deref
(fn(∀ '(α, β), ∅; &shr{α}(ref β ty)) → &shr{α}ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x').
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -145,7 +145,7 @@ Section ref_functions.
Lemma ref_drop_type ty `{!TyWf ty} :
typed_val ref_drop (fn(∀ α, ∅; ref α ty) → unit).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL Hk Hx". rewrite tctx_interp_singleton tctx_hasty_val.
destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
@@ -210,7 +210,7 @@ Section ref_functions.
typed_val call_once (fn(∀ α, ∅; fty, &shr{α}ty1) → &shr{α}ty2) →
typed_val (ref_map call_once) (fn(∀ α, ∅; ref α ty1, fty) → ref α ty2).
Proof.
- intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg).
inv_vec arg=>ref env. simpl_subst.
iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
@@ -289,7 +289,7 @@ Section ref_functions.
typed_val (ref_map_split call_once)
(fn(∀ α, ∅; ref α ty, fty) → Π[ref α ty1; ref α ty2]).
Proof.
- intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg).
inv_vec arg=>ref env. simpl_subst.
iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 23ad8be5..c56f81a0 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -76,11 +76,11 @@ Section refcell_inv.
(* TODO : this proof is essentially [solve_proper], but within the logic. *)
(* It would easily gain from some automation. *)
rewrite eqtype_unfold. iIntros (Hty) "HL".
- iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
+ iDestruct (Hty with "HL") as "#Hty". iIntros "* !> #HE H".
iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
&{α}((l +ₗ 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
- { iIntros "!# H". iApply bor_iff; last done.
+ { iIntros "!> H". iApply bor_iff; last done.
iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
iFrame; by iApply "Hown". }
iDestruct "H" as (st) "H"; iExists st;
@@ -187,8 +187,8 @@ Section refcell.
iDestruct (EQ' with "HL") as "#EQ'".
iDestruct (refcell_inv_proper with "HL") as "#Hty1ty2"; first done.
iDestruct (refcell_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
- iIntros "!# #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
- iSplit; [|iSplit; iIntros "!# * H"].
+ iIntros "!> #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
+ iSplit; [|iSplit; iIntros "!> * H"].
- iPureIntro. simpl. congruence.
- destruct vl as [|[[]|]]=>//=. by iApply "Hown".
- simpl. iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index c494d485..40277f10 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -21,7 +21,7 @@ Section refcell_functions.
Lemma refcell_new_type ty `{!TyWf ty} :
typed_val (refcell_new ty) (fn(∅; ty) → refcell ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new (S ty.(ty_size))); [solve_typing..|].
iIntros (r tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -55,7 +55,7 @@ Section refcell_functions.
Lemma refcell_into_inner_type ty `{!TyWf ty} :
typed_val (refcell_into_inner ty) (fn(∅; refcell ty) → ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new ty.(ty_size)); [solve_typing..|].
iIntros (r tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -88,7 +88,7 @@ Section refcell_functions.
typed_val refcell_get_mut
(fn(∀ α, ∅; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL HC HT".
@@ -140,12 +140,12 @@ Section refcell_functions.
typed_val refcell_try_borrow
(fn(∀ α, ∅; &shr{α}(refcell ty)) → option (ref α ty)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply (type_cont [] [Ï âŠ‘â‚— []] (λ _, [x â— box (&shr{α}(refcell ty));
r ◠box (option (ref α ty))]));
- [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg]; simpl_subst; last first.
+ [iIntros (k)|iIntros "/= !>"; iIntros (k arg); inv_vec arg]; simpl_subst; last first.
{ iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
iApply type_deref; [solve_typing..|].
@@ -249,12 +249,12 @@ Section refcell_functions.
typed_val refcell_try_borrow_mut
(fn(∀ α, ∅; &shr{α}(refcell ty)) → option (refmut α ty))%T.
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply (type_cont [] [Ï âŠ‘â‚— []] (λ _, [x â— box (&shr{α}(refcell ty));
r ◠box (option (refmut α ty))]));
- [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
+ [iIntros (k)|iIntros "/= !>"; iIntros (k arg); inv_vec arg];
simpl_subst; last first.
{ iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 9a0be7e7..a435bbda 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -66,7 +66,7 @@ Section refmut.
iIntros (??????) "#? H". iDestruct "H" as (lv lrc) "[#Hf #H]".
iExists _, _. iSplit.
- by iApply frac_bor_shorten.
- - iIntros "!# * % Htok".
+ - iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
{ iApply lft_intersect_mono. iApply lft_incl_refl. done. }
iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
@@ -87,7 +87,7 @@ Section refmut.
Proof.
intros α1 α2 Hα ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (qmax qL) "HL".
iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
- iIntros "!# #HE". iDestruct ("Hα" with "HE") as %Hα1α2.
+ iIntros "!> #HE". iDestruct ("Hα" with "HE") as %Hα1α2.
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
- done.
- iIntros (tid [|[[]|][|[[]|][]]]) "H"=>//=.
@@ -100,7 +100,7 @@ Section refmut.
iExists vl; iFrame; by iApply "Ho".
+ iApply lft_incl_trans; last done. by iApply lft_incl_syn_sem.
- iIntros (κ tid l) "H /=". iDestruct "H" as (lv lrc) "H". iExists lv, lrc.
- iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
+ iDestruct "H" as "[$ #H]". iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
{ iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl. }
iMod ("H" with "[] Htok") as "Hshr"; first done. iModIntro. iNext.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 23e1ce16..8d8514d3 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -20,7 +20,7 @@ Section refmut_functions.
Lemma refmut_deref_type ty `{!TyWf ty} :
typed_val refmut_deref (fn(∀ '(α, β), ∅; &shr{α}(refmut β ty)) → &shr{α}ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x').
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -58,7 +58,7 @@ Section refmut_functions.
typed_val refmut_derefmut
(fn(∀ '(α, β), ∅; &uniq{α}(refmut β ty)) → &uniq{α}ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x').
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -113,7 +113,7 @@ Section refmut_functions.
Lemma refmut_drop_type ty `{!TyWf ty} :
typed_val refmut_drop (fn(∀ α, ∅; refmut α ty) → unit).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL Hk Hx". rewrite tctx_interp_singleton tctx_hasty_val.
destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
@@ -181,7 +181,7 @@ Section refmut_functions.
typed_val call_once (fn(∀ α, ∅; fty, &uniq{α}ty1) → &uniq{α}ty2) →
typed_val (refmut_map call_once) (fn(∀ α, ∅; refmut α ty1, fty) → refmut α ty2).
Proof.
- intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg).
inv_vec arg=>ref env. simpl_subst.
iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
@@ -260,7 +260,7 @@ Section refmut_functions.
typed_val (refmut_map_split call_once)
(fn(∀ α, ∅; refmut α ty, fty) → Π[refmut α ty1; refmut α ty2]).
Proof.
- intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg).
inv_vec arg=>refmut env. simpl_subst.
iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index c462ce0b..414c8651 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -69,11 +69,11 @@ Section rwlock_inv.
(* TODO : this proof is essentially [solve_proper], but within the logic.
It would easily gain from some automation. *)
rewrite eqtype_unfold. iIntros (Hty) "HL".
- iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
+ iDestruct (Hty with "HL") as "#Hty". iIntros "* !> #HE H".
iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid_own) -∗
&{α}((l +ₗ 1) ↦∗: ty_own ty2 tid_own)))%I as "#Hb".
- { iIntros "!# H". iApply bor_iff; last done.
+ { iIntros "!> H". iApply bor_iff; last done.
iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
iFrame; by iApply "Hown". }
iDestruct "H" as (st) "H"; iExists st;
@@ -194,8 +194,8 @@ Section rwlock.
iDestruct (EQ' with "HL") as "#EQ'".
iDestruct (rwlock_inv_proper with "HL") as "#Hty1ty2"; first done.
iDestruct (rwlock_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
- iIntros "!# #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
- iSplit; [|iSplit; iIntros "!# * H"].
+ iIntros "!> #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
+ iSplit; [|iSplit; iIntros "!> * H"].
- iPureIntro. simpl. congruence.
- destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
- iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 41bd404c..f12aad29 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -21,7 +21,7 @@ Section rwlock_functions.
Lemma rwlock_new_type ty `{!TyWf ty} :
typed_val (rwlock_new ty) (fn(∅; ty) → rwlock ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new (S ty.(ty_size))); [solve_typing..|].
iIntros (r tid qmax) "#LFT HE Hna HL Hk HT". simpl_subst.
@@ -56,7 +56,7 @@ Section rwlock_functions.
Lemma rwlock_into_inner_type ty `{!TyWf ty} :
typed_val (rwlock_into_inner ty) (fn(∅; rwlock ty) → ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_new ty.(ty_size)); [solve_typing..|].
iIntros (r tid qmax) "#LFT HE Hna HL Hk HT". simpl_subst.
@@ -89,7 +89,7 @@ Section rwlock_functions.
Lemma rwlock_get_mut_type ty `{!TyWf ty} :
typed_val rwlock_get_mut (fn(∀ α, ∅; &uniq{α} (rwlock ty)) → &uniq{α} ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
iIntros (tid qmax) "#LFT HE Hna HL HC HT".
@@ -140,18 +140,18 @@ Section rwlock_functions.
typed_val rwlock_try_read
(fn(∀ α, ∅; &shr{α}(rwlock ty)) → option (rwlockreadguard α ty)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
iApply (type_cont [] [Ï âŠ‘â‚— []] (λ _, [x â— box (&shr{α}(rwlock ty));
r ◠box (option (rwlockreadguard α ty))]));
- [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
+ [iIntros (k)|iIntros "/= !>"; iIntros (k arg); inv_vec arg];
simpl_subst; last first.
{ iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
iApply (type_cont [] [Ï âŠ‘â‚— []] (λ _, [x â— _; x' â— _; r â— _]));
- [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
+ [iIntros (loop)|iIntros "/= !>"; iIntros (loop arg); inv_vec arg];
simpl_subst.
{ iApply type_jump; solve_typing. }
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
@@ -253,11 +253,11 @@ Section rwlock_functions.
typed_val rwlock_try_write
(fn(∀ α, ∅; &shr{α}(rwlock ty)) → option (rwlockwriteguard α ty)).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply (type_cont [_] [Ï âŠ‘â‚— []] (λ r, [x â— box (&shr{α}(rwlock ty));
(r!!!0%fin:val) ◠box (option (rwlockwriteguard α ty))]));
- [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
+ [iIntros (k)|iIntros "/= !>"; iIntros (k arg); inv_vec arg=>r];
simpl_subst; last first.
{ iApply type_delete; [solve_typing..|]. iApply type_jump; solve_typing. }
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index e39ef044..cb771c83 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -83,7 +83,7 @@ Section rwlockreadguard.
iDestruct (proj1 Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
iDestruct (rwlock_inv_proper with "HL") as "#Hty1ty2"; first done.
iDestruct (rwlock_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
- iIntros "!# #HE". iDestruct ("Hα" with "HE") as %Hα1α2.
+ iIntros "!> #HE". iDestruct ("Hα" with "HE") as %Hα1α2.
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
- done.
- iIntros (tid [|[[]|][]]) "H"; try done.
@@ -93,7 +93,7 @@ Section rwlockreadguard.
iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
+ iApply lft_incl_trans; first by iApply lft_incl_syn_sem. done.
+ iApply (at_bor_iff with "[] Hinv").
- iIntros "!> !#"; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1".
+ iIntros "!> !>"; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1".
- iIntros (κ tid l) "H". iDestruct "H" as (l') "[Hf Hshr]". iExists l'.
iFrame. iApply ty_shr_mono; last by iApply "Hs".
iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index f6dccc46..c8ab78fc 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -21,7 +21,7 @@ Section rwlockreadguard_functions.
typed_val rwlockreadguard_deref
(fn(∀ '(α, β), ∅; &shr{α}(rwlockreadguard β ty)) → &shr{α} ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x').
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -61,11 +61,11 @@ Section rwlockreadguard_functions.
Lemma rwlockreadguard_drop_type ty `{!TyWf ty} :
typed_val rwlockreadguard_drop (fn(∀ α, ∅; rwlockreadguard α ty) → unit).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
iApply (type_cont [] [Ï âŠ‘â‚— []] (λ _, [x â— _; x' â— _]));
- [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
+ [iIntros (loop)|iIntros "/= !>"; iIntros (loop arg); inv_vec arg];
simpl_subst.
{ iApply type_jump; solve_typing. }
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 5b348f3d..7bffa2d3 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -54,7 +54,7 @@ Section rwlockwriteguard.
iIntros (??????) "#? H". iDestruct "H" as (l') "[#Hf #H]".
iExists _. iSplit.
- by iApply frac_bor_shorten.
- - iIntros "!# * % Htok".
+ - iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
{ iApply lft_intersect_mono. iApply lft_incl_refl. done. }
iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
@@ -82,7 +82,7 @@ Section rwlockwriteguard.
iDestruct (Hty' with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
iDestruct (rwlock_inv_proper with "HL") as "#Hty1ty2"; first done.
iDestruct (rwlock_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
- iIntros "!# #HE". iDestruct ("Hα" with "HE") as %Hα1α2.
+ iIntros "!> #HE". iDestruct ("Hα" with "HE") as %Hα1α2.
iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
- done.
- iIntros (tid [|[[]|][]]) "H"; try done.
@@ -93,9 +93,9 @@ Section rwlockwriteguard.
iExists vl; iFrame; by iApply "Ho".
+ iApply lft_incl_trans; first by iApply lft_incl_syn_sem. done.
+ iApply at_bor_iff; try done.
- iIntros "!>!#"; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1".
+ iIntros "!>!>"; iSplit; iIntros "H". by iApply "Hty1ty2". by iApply "Hty2ty1".
- iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
- iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
+ iDestruct "H" as "[$ #H]". iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
{ iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl. }
iMod ("H" with "[] Htok") as "Hshr"; first done. iModIntro. iNext.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 9ff16886..c529dfec 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -21,7 +21,7 @@ Section rwlockwriteguard_functions.
typed_val rwlockwriteguard_deref
(fn(∀ '(α, β), ∅; &shr{α}(rwlockwriteguard β ty)) → &shr{α} ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x').
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -66,7 +66,7 @@ Section rwlockwriteguard_functions.
typed_val rwlockwriteguard_derefmut
(fn(∀ '(α, β), ∅; &uniq{α}(rwlockwriteguard β ty)) → &uniq{α}ty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros ([α β] Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x').
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
@@ -112,7 +112,7 @@ Section rwlockwriteguard_functions.
typed_val rwlockwriteguard_drop
(fn(∀ α, ∅; rwlockwriteguard α ty) → unit).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT".
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index a546ad15..569cf557 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -33,7 +33,7 @@ Section join_handle.
iIntros "#Hincl". iSplit; first done. iSplit; iModIntro.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
simpl. iApply (join_handle_impl with "[] Hvl"). clear tid.
- iIntros "!# * Hown" (tid).
+ iIntros "!> * Hown" (tid).
iDestruct (box_type_incl with "Hincl") as "{Hincl} (_ & Hincl & _)".
iApply "Hincl". done.
- iIntros "* _". auto.
@@ -43,7 +43,7 @@ Section join_handle.
Proper (subtype E L ==> subtype E L) join_handle.
Proof.
iIntros (ty1 ty2 Hsub ??) "HL". iDestruct (Hsub with "HL") as "#Hsub".
- iIntros "!# #HE". iApply join_handle_subtype. iApply "Hsub"; done.
+ iIntros "!> #HE". iApply join_handle_subtype. iApply "Hsub"; done.
Qed.
Global Instance join_handle_proper E L :
Proper (eqtype E L ==> eqtype E L) join_handle.
@@ -82,7 +82,7 @@ Section spawn.
let E Ï := ty_outlives_E fty static ++ ty_outlives_E retty static in
typed_val (spawn call_once) (fn(E; fty) → join_handle retty).
Proof.
- intros Hf ? E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros Hf ? E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>env. simpl_subst.
iApply type_let; [apply Hf|solve_typing|]. iIntros (f'). simpl_subst.
iApply (type_let _ _ _ _ ([f' â— _; env â— _])
@@ -116,7 +116,7 @@ Section spawn.
Lemma join_type retty `{!TyWf retty} :
typed_val join (fn(∅; join_handle retty) → retty).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (_ Ï ret arg). inv_vec arg=>c. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (c'); simpl_subst.
iApply (type_let _ _ _ _ ([c' â— _])
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index e76b730c..70033108 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -17,7 +17,7 @@ Section swap.
Lemma swap_type Ï„ `{!TyWf Ï„} :
typed_val (swap τ) (fn(∀ α, ∅; &uniq{α} τ, &uniq{α} τ) → unit).
Proof.
- intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α Ï ret p).
+ intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>". iIntros (α Ï ret p).
inv_vec p=>p1 p2. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (p1'). simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (p2'). simpl_subst.
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 7acd8b79..95337871 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -23,7 +23,7 @@ Section code.
typed_val call_once (fn(∅; fty, ty) → ty) →
typed_val (take ty call_once) (fn(∀ α, ∅; &uniq{α} ty, fty) → unit).
Proof.
- intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+ intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (α Ï ret arg). inv_vec arg=>x env. simpl_subst.
iApply type_deref; [solve_typing..|]; iIntros (x'); simpl_subst.
iApply type_let; [apply Hf|solve_typing|]; iIntros (f'); simpl_subst.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 2d246eb1..0c345c96 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -78,7 +78,7 @@ Section own.
Next Obligation.
intros _ ty κ κ' tid l. iIntros "#Hκ #H".
iDestruct "H" as (l') "[Hfb #Hvs]".
- iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!# *% Htok".
+ iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!> *% Htok".
iApply (step_fupd_mask_mono F _ (F∖↑shrN)); [solve_ndisj..|].
iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
@@ -98,7 +98,7 @@ Section own.
iDestruct "Heq" as %->. iFrame. iApply (heap_mapsto_pred_wand with "Hmt").
iApply "Ho".
- iIntros (???) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
- iExists l'. iFrame. iIntros "!#". iIntros (F' q) "% Htok".
+ iExists l'. iFrame. iIntros "!>". iIntros (F' q) "% Htok".
iMod ("Hvs" with "[%] Htok") as "Hvs'". done. iModIntro. iNext.
iMod "Hvs'" as "[Hshr $]". iApply ("Hs" with "Hshr").
Qed.
@@ -108,7 +108,7 @@ Section own.
Proof.
intros ty1 ty2 Hincl. iIntros (qmax qL) "HL".
iDestruct (Hincl with "HL") as "#Hincl".
- iClear "∗". iIntros "!# #HE".
+ iClear "∗". iIntros "!> #HE".
iApply own_type_incl; first by auto. iApply "Hincl"; auto.
Qed.
Lemma own_mono' E L n1 n2 ty1 ty2 :
@@ -162,7 +162,7 @@ Section box.
Proof.
intros ty1 ty2 Hincl. iIntros (qmax qL) "HL".
iDestruct (Hincl with "HL") as "#Hincl".
- iClear "∗". iIntros "!# #HE".
+ iClear "∗". iIntros "!> #HE".
iApply box_type_incl. iApply "Hincl"; auto.
Qed.
Lemma box_mono' E L ty1 ty2 :
@@ -220,7 +220,7 @@ Section typing.
Lemma write_own {E L} ty ty' n :
ty.(ty_size) = ty'.(ty_size) → ⊢ typed_write E L (own_ptr n ty') ty (own_ptr n ty).
Proof.
- rewrite typed_write_eq. iIntros (Hsz) "!#".
+ rewrite typed_write_eq. iIntros (Hsz) "!>".
iIntros ([[]|] tid F qmax qL ?) "_ _ $ Hown"; try done.
rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%". iExists _, _. iFrame "H↦". auto.
@@ -229,7 +229,7 @@ Section typing.
Lemma read_own_copy E L ty n :
Copy ty → ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n ty).
Proof.
- rewrite typed_read_eq. iIntros (Hsz) "!#".
+ rewrite typed_read_eq. iIntros (Hsz) "!>".
iIntros ([[]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iExists l, _, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !>".
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 60503985..59ef6191 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -91,7 +91,7 @@ Section product.
Proof.
iIntros (ty11 ty12 H1 ty21 ty22 H2). iIntros (qmax qL) "HL".
iDestruct (H1 with "HL") as "#H1". iDestruct (H2 with "HL") as "#H2".
- iClear "∗". iIntros "!# #HE".
+ iClear "∗". iIntros "!> #HE".
iDestruct ("H1" with "HE") as "#(% & #Ho1 & #Hs1)". clear H1.
iDestruct ("H2" with "HE") as "#(% & #Ho2 & #Hs2)". clear H2.
iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iModIntro.
@@ -199,8 +199,8 @@ Section typing.
Global Instance prod2_assoc E L : Assoc (eqtype E L) product2.
Proof.
- intros ???. apply eqtype_unfold. iIntros (??) "_ !# _".
- iSplit; first by rewrite /= assoc. iSplit; iIntros "!# *"; iSplit; iIntros "H".
+ intros ???. apply eqtype_unfold. iIntros (??) "_ !> _".
+ iSplit; first by rewrite /= assoc. iSplit; iIntros "!> *"; iSplit; iIntros "H".
- iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
iExists _, _. iSplit. by rewrite assoc. iFrame. iExists _, _. by iFrame.
@@ -215,8 +215,8 @@ Section typing.
Global Instance prod2_unit_leftid E L : LeftId (eqtype E L) unit product2.
Proof.
- intros ty. apply eqtype_unfold. iIntros (??) "_ !# _". iSplit; first done.
- iSplit; iIntros "!# *"; iSplit; iIntros "H".
+ intros ty. apply eqtype_unfold. iIntros (??) "_ !> _". iSplit; first done.
+ iSplit; iIntros "!> *"; iSplit; iIntros "H".
- iDestruct "H" as (? ?) "(% & % & ?)". by subst.
- iExists [], _. eauto.
- iDestruct "H" as "(? & ?)". rewrite shift_loc_0.
@@ -227,8 +227,8 @@ Section typing.
Global Instance prod2_unit_rightid E L : RightId (eqtype E L) unit product2.
Proof.
- intros ty. apply eqtype_unfold. iIntros (??) "_ !# _".
- iSplit; first by rewrite /= -plus_n_O. iSplit; iIntros "!# *"; iSplit; iIntros "H".
+ intros ty. apply eqtype_unfold. iIntros (??) "_ !> _".
+ iSplit; first by rewrite /= -plus_n_O. iSplit; iIntros "!> *"; iSplit; iIntros "H".
- iDestruct "H" as (? ?) "(% & ? & %)". subst. by rewrite app_nil_r.
- iExists _, []. rewrite app_nil_r. eauto.
- iDestruct "H" as "(? & _)". done.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 220bd01c..8b387f12 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -307,7 +307,7 @@ Section typing_rules.
{{{ RET #☠; na_own tid ⊤ ∗ llctx_interp_noend qmax L qL ∗
tctx_elt_interp tid (p1 ◠ty1') ∗ tctx_elt_interp tid (p2 ◠ty2') }}}.
Proof.
- iIntros (<-) "#Hwrt #Hread !#".
+ iIntros (<-) "#Hwrt #Hread !>".
iIntros (Φ) "(#LFT & #HE & Htl & [HL1 HL2] & [Hp1 Hp2]) HΦ".
wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "% Hown2".
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 471a6775..e6042d95 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -22,7 +22,7 @@ Section shr_bor.
κ2 ⊑ κ1 -∗ type_incl ty1 ty2 -∗ type_incl (shr_bor κ1 ty1) (shr_bor κ2 ty2).
Proof.
iIntros "#Hκ #[_ [_ Hty]]". iApply type_incl_simple_type. simpl.
- iIntros "!#" (tid [|[[]|][]]) "H"; try done. iApply "Hty".
+ iIntros "!>" (tid [|[[]|][]]) "H"; try done. iApply "Hty".
iApply (ty1.(ty_shr_mono) with "Hκ"). done.
Qed.
@@ -31,7 +31,7 @@ Section shr_bor.
Proof.
intros κ1 κ2 Hκ ty1 ty2 Hty.
iIntros (??) "/= HL". iDestruct (Hκ with "HL") as "#Hincl".
- iDestruct (Hty with "HL") as "#Hty". iIntros "!# #HE".
+ iDestruct (Hty with "HL") as "#Hty". iIntros "!> #HE".
iDestruct ("Hincl" with "HE") as "%".
iApply shr_type_incl.
- by iApply lft_incl_syn_sem.
@@ -86,7 +86,7 @@ Section typing.
Lemma read_shr E L κ ty :
Copy ty → lctx_lft_alive E L κ → ⊢ typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
Proof.
- rewrite typed_read_eq. iIntros (Hcopy Halive) "!#".
+ rewrite typed_read_eq. iIntros (Hcopy Halive) "!>".
iIntros ([[]|] tid F qmax qL ?) "#LFT #HE Htl HL #Hshr"; try done.
iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first solve_ndisj.
iMod (copy_shr_acc with "LFT Hshr Htl Hκ") as (q') "(Htl & H↦ & Hcl)"; first solve_ndisj.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 82f1a461..991d199f 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -129,12 +129,12 @@ Section sum.
iIntros (tyl1 tyl2 Htyl qmax qL) "HL".
iAssert (â–¡ (elctx_interp E -∗ ⌜max_list_with ty_size tyl1 = max_list_with ty_size tyl2âŒ))%I with "[#]" as "#Hleq".
{ iInduction Htyl as [|???? Hsub] "IH".
- { iClear "∗". iIntros "!# _". done. }
+ { iClear "∗". iIntros "!> _". done. }
iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH".
iModIntro. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)".
iDestruct ("IH" with "HE") as %IH. iPureIntro. simpl. inversion_clear IH. by f_equal. }
iDestruct (subtype_Forall2_llctx_noend with "HL") as "#Htyl"; first done.
- iClear "HL". iIntros "!# #HE".
+ iClear "HL". iIntros "!> #HE".
iDestruct ("Hleq" with "HE") as %Hleq. iSpecialize ("Htyl" with "HE"). iClear "Hleq HE".
iAssert (∀ i, type_incl (nth i tyl1 emp0) (nth i tyl2 emp0))%I with "[#]" as "#Hty".
{ iIntros (i). edestruct (nth_lookup_or_length tyl1 i) as [Hl1|Hl]; last first.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 384c1089..a943dab5 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -580,14 +580,14 @@ Section subtyping.
Qed.
Lemma subtype_refl E L ty : subtype E L ty ty.
- Proof. iIntros (??) "_ !# _". iApply type_incl_refl. Qed.
+ Proof. iIntros (??) "_ !> _". iApply type_incl_refl. Qed.
Global Instance subtype_preorder E L : PreOrder (subtype E L).
Proof.
split; first by intros ?; apply subtype_refl.
iIntros (ty1 ty2 ty3 H12 H23 ??) "HL".
iDestruct (H12 with "HL") as "#H12".
iDestruct (H23 with "HL") as "#H23".
- iClear "∗". iIntros "!# #HE".
+ iClear "∗". iIntros "!> #HE".
iApply (type_incl_trans with "[#]"). by iApply "H12". by iApply "H23".
Qed.
@@ -602,8 +602,8 @@ Section subtyping.
{ iApply big_sepL_forall. iIntros (k [ty1 ty2] Hlookup).
move:Htys => /Forall2_Forall /Forall_forall=>Htys.
iApply (Htys (ty1, ty2)); first by exact: elem_of_list_lookup_2. done. }
- iClear "∗". iIntros "!# #HE". iApply (big_sepL_impl with "[$Htys]").
- iIntros "!# * % #Hincl". by iApply "Hincl".
+ iClear "∗". iIntros "!> #HE". iApply (big_sepL_impl with "[$Htys]").
+ iIntros "!> * % #Hincl". by iApply "Hincl".
Qed.
Lemma subtype_Forall2_llctx E L tys1 tys2 qmax :
@@ -673,24 +673,24 @@ Section subtyping.
- iIntros ([EQ1 EQ2] qmax qL) "HL".
iDestruct (EQ1 with "HL") as "#EQ1".
iDestruct (EQ2 with "HL") as "#EQ2".
- iClear "∗". iIntros "!# #HE".
+ iClear "∗". iIntros "!> #HE".
iDestruct ("EQ1" with "HE") as "[#Hsz [#H1own #H1shr]]".
iDestruct ("EQ2" with "HE") as "[_ [#H2own #H2shr]]".
iSplit; last iSplit.
+ done.
- + by iIntros "!#*"; iSplit; iIntros "H"; [iApply "H1own"|iApply "H2own"].
- + by iIntros "!#*"; iSplit; iIntros "H"; [iApply "H1shr"|iApply "H2shr"].
+ + by iIntros "!>*"; iSplit; iIntros "H"; [iApply "H1own"|iApply "H2own"].
+ + by iIntros "!>*"; iSplit; iIntros "H"; [iApply "H1shr"|iApply "H2shr"].
- intros EQ. split; (iIntros (qmax qL) "HL";
iDestruct (EQ with "HL") as "#EQ";
- iClear "∗"; iIntros "!# #HE";
+ iClear "∗"; iIntros "!> #HE";
iDestruct ("EQ" with "HE") as "[% [#Hown #Hshr]]";
(iSplit; last iSplit)).
+ done.
- + iIntros "!#* H". by iApply "Hown".
- + iIntros "!#* H". by iApply "Hshr".
+ + iIntros "!>* H". by iApply "Hown".
+ + iIntros "!>* H". by iApply "Hshr".
+ done.
- + iIntros "!#* H". by iApply "Hown".
- + iIntros "!#* H". by iApply "Hshr".
+ + iIntros "!>* H". by iApply "Hown".
+ + iIntros "!>* H". by iApply "Hshr".
Qed.
Lemma eqtype_refl E L ty : eqtype E L ty ty.
@@ -727,8 +727,8 @@ Section subtyping.
subtype E L st1 st2.
Proof.
intros Hst. iIntros (qmax qL) "HL". iDestruct (Hst with "HL") as "#Hst".
- iClear "∗". iIntros "!# #HE". iApply type_incl_simple_type.
- iIntros "!#" (??) "?". by iApply "Hst".
+ iClear "∗". iIntros "!> #HE". iApply type_incl_simple_type.
+ iIntros "!>" (??) "?". by iApply "Hst".
Qed.
Lemma subtype_weaken E1 E2 L1 L2 ty1 ty2 :
@@ -737,7 +737,7 @@ Section subtyping.
Proof.
iIntros (HE12 ? Hsub qmax qL) "HL". iDestruct (Hsub with "[HL]") as "#Hsub".
{ rewrite /llctx_interp. by iApply big_sepL_submseteq. }
- iClear "∗". iIntros "!# #HE". iApply "Hsub".
+ iClear "∗". iIntros "!> #HE". iApply "Hsub".
rewrite /elctx_interp. by iApply big_sepL_submseteq.
Qed.
End subtyping.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index bddc9622..e45318a9 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -42,7 +42,7 @@ Section uninit.
Next Obligation. iIntros (???) "%". done. Qed.
Next Obligation.
iIntros (???????) "LFT Hvl". iApply (ty_share (uninit0 n) with "LFT"); first done.
- iApply (bor_iff with "[] Hvl"). iIntros "!> !#". setoid_rewrite uninit0_own.
+ iApply (bor_iff with "[] Hvl"). iIntros "!> !>". setoid_rewrite uninit0_own.
iSplit; iIntros; done.
Qed.
Next Obligation. intros. by apply ty_shr_mono. Qed.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index badff4b2..674d69f5 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -34,7 +34,7 @@ Section uniq_bor.
iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⊓κ' ⊑ κ0⊓κ)%I as "#Hκ0".
{ iApply lft_intersect_mono. iApply lft_incl_refl. done. }
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
- iIntros "!# * % Htok". iApply (step_fupd_mask_mono F _ (F∖↑shrN)); try solve_ndisj.
+ iIntros "!> * % Htok". iApply (step_fupd_mask_mono F _ (F∖↑shrN)); try solve_ndisj.
iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
@@ -59,7 +59,7 @@ Section uniq_bor.
iExists vl; iFrame; by iApply "Hty".
- iIntros (κ ??) "H". iAssert (κ2 ⊓ κ ⊑ κ1 ⊓ κ)%I as "#Hincl'".
{ iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
- iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!# %%% Htok".
+ iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!> %%% Htok".
iMod (lft_incl_acc with "Hincl' Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hupd" with "[%] Htok") as "Hupd'"; try done. iModIntro. iNext.
iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
@@ -73,7 +73,7 @@ Section uniq_bor.
Proof.
intros κ1 κ2 Hκ ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (??) "HL".
iDestruct (Hty with "HL") as "#Hty". iDestruct (Hκ with "HL") as "#Hκ".
- iIntros "!# #HE".
+ iIntros "!> #HE".
iApply uniq_type_incl.
- iDestruct ("Hκ" with "HE") as %H.
apply lft_incl_syn_sem in H. iApply H.
@@ -147,7 +147,7 @@ Section typing.
Lemma read_uniq E L κ ty :
Copy ty → lctx_lft_alive E L κ → ⊢ typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
- rewrite typed_read_eq. iIntros (Hcopy Halive) "!#".
+ rewrite typed_read_eq. iIntros (Hcopy Halive) "!>".
iIntros ([[]|] tid F qmax qL ?) "#LFT #HE Htl HL Hown"; try done.
iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first solve_ndisj.
iMod (bor_acc with "LFT Hown Hκ") as "[H↦ Hclose']"; first solve_ndisj.
@@ -161,7 +161,7 @@ Section typing.
Lemma write_uniq E L κ ty :
lctx_lft_alive E L κ → ⊢ typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
Proof.
- rewrite typed_write_eq. iIntros (Halive) "!#".
+ rewrite typed_write_eq. iIntros (Halive) "!>".
iIntros ([[]|] tid F qmax qL ?) "#LFT HE HL Hown"; try done.
iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
iMod (bor_acc with "LFT Hown Htok") as "[H↦ Hclose']"; first solve_ndisj.
diff --git a/theories/typing/util.v b/theories/typing/util.v
index c120c7ba..857d6a42 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -34,7 +34,7 @@ Section util.
iDestruct "Hbor" as (i) "(#Hpb&Hpbown)".
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty κ tid l)%I
with "[Hpbown]") as "#Hinv"; first by eauto.
- iIntros "!> !# * % Htok".
+ iIntros "!> !> * % Htok".
iMod (inv_acc with "Hinv") as "[INV Hclose]"; first solve_ndisj.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iMod (bor_later_tok with "LFT [Hbtok] Htok") as "Hdelay"; first solve_ndisj.
@@ -56,7 +56,7 @@ Section util.
iDestruct "Hbor" as (i) "(#Hpb&Hpbown)".
iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty κ'' tid l)%I
with "[Hpbown]") as "#Hinv"; first by eauto.
- iIntros "!> !# * % Htok".
+ iIntros "!> !> * % Htok".
iMod (inv_acc with "Hinv") as "[INV Hclose]"; first solve_ndisj.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iMod (bor_unnest with "LFT [Hbtok]") as "Hb"; first solve_ndisj.
--
GitLab