From da96d24688a68fa59231424d4a860b840f49be9c Mon Sep 17 00:00:00 2001
From: Hai Dang <hai@bedrocksystems.com>
Date: Sun, 7 May 2023 20:33:56 +0200
Subject: [PATCH] update dependencies

---
 coq-lambda-rust.opam                   |  2 +-
 theories/lifetime/model/accessors.v    |  2 +-
 theories/lifetime/model/borrow.v       |  2 +-
 theories/lifetime/model/creation.v     |  4 ++--
 theories/lifetime/model/faking.v       |  2 +-
 theories/lifetime/model/reborrow.v     |  2 +-
 theories/typing/borrow.v               |  2 +-
 theories/typing/examples/nonlexical.v  |  2 +-
 theories/typing/lib/arc.v              | 14 +++++++-------
 theories/typing/lib/diverging_static.v |  4 ++--
 theories/typing/lib/mutex/mutex.v      |  2 +-
 theories/typing/lib/panic.v            |  2 +-
 theories/typing/lib/rc/rc.v            |  4 ++--
 theories/typing/lib/rc/weak.v          |  4 ++--
 theories/typing/lib/refcell/refcell.v  |  8 ++++----
 theories/typing/lib/rwlock/rwlock.v    |  6 +++---
 theories/typing/lib/spawn.v            |  2 +-
 theories/typing/own.v                  |  6 +++---
 theories/typing/product_split.v        | 14 +++++++-------
 theories/typing/type.v                 |  6 +++---
 theories/typing/type_context.v         | 16 ++++++++++------
 theories/typing/type_sum.v             |  7 ++++---
 theories/typing/uninit.v               |  2 +-
 theories/typing/uniq_bor.v             |  2 +-
 theories/typing/util.v                 |  4 ++--
 25 files changed, 63 insertions(+), 58 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index aacd92be..472a350a 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2023-05-03.1.44a343ae") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2023-05-07.0.9cf7aca0") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index e7b59778..2653421e 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -111,7 +111,7 @@ Proof.
           by setoid_subst.
         + apply (inj Some) in HA'. inversion HA'.
         + inversion HA'.
-      - rewrite lookup_fmap in HA'. destruct (A'!!Λ) as [[]|]; [|by inversion HA'].
+      - rewrite lookup_fmap in HA'. destruct (A'!!Λ) as [[b l]|]; [|by inversion HA'].
         apply (inj Some) in HA'. setoid_subst. apply csum_included in Hs.
         destruct b, Hs as [[=]|[(?&?&[=]&[=]&[_ Hincl%latT_included]%prod_included)|
           (?&?&[=]&?)]]. auto with subst. }
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index afb8da0b..6bb73e53 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 From iris.prelude Require Import options.
 
 Section borrow.
-Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
+Context `{!invGS Σ, !lftG Σ Lat userE, !@LatBottom Lat bot}.
 Implicit Types κ : lft.
 
 Local Set Default Proof Using "Type*".
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 00e13c7e..2281b1a7 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 From iris.prelude Require Import options.
 
 Section creation.
-Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
+Context `{!invGS Σ, !lftG Σ Lat userE, !@LatBottom Lat bot}.
 Implicit Types κ : lft.
 
 Local Set Default Proof Using "Type*".
@@ -27,7 +27,7 @@ Proof.
   rewrite /lft_bor_alive; iDestruct "Hbor" as (B) "[[Hbox Hbor] HB]".
   iAssert ⌜∀ i s, B !! i = Some s → ∃ V, s = Bor_in V ∧ V ⊑ (Vs κ)⌝%I with "[#]" as %HB.
   { iIntros (i s HBI). rewrite (big_sepM_lookup _ B) //.
-    destruct s as [V|q|κ']; rewrite /bor_cnt; [iExists _; by iSplit| |].
+    destruct s as [V|q Vtok V|κ']; rewrite /bor_cnt; [iExists _; by iSplit| |].
     { iDestruct "HB" as "[_ HB]". iDestruct "Hκ" as (Vκ) "Hκ".
       set (V' := Vtok ⊔ Vκ).
       iDestruct (lft_tok_dead $! V' with "HB Hκ") as "[]". }
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 8f9598c8..4c7d0168 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -65,7 +65,7 @@ Proof.
         + rewrite !option_guard_False; set_solver. }
     eapply op_local_update_discrete=>HA Λ. specialize (HA Λ).
     rewrite lookup_op lookup_gset_to_gmap !lookup_fmap.
-    destruct (A !! Λ) eqn:EQ.
+    destruct (A !! Λ) as [p|] eqn:EQ.
     - apply elem_of_dom_2 in EQ.
       rewrite option_guard_False; [by destruct p as [[]?]|set_solver].
     - apply not_elem_of_dom in EQ.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 9a2c56b9..ac1c65d0 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -32,7 +32,7 @@ Proof.
 Qed.
 
 Section reborrow.
-Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
+Context `{!invGS Σ, !lftG Σ Lat userE, !@LatBottom Lat bot}.
 Implicit Types κ : lft.
 
 Local Set Default Proof Using "Type*".
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 602de0b8..7646e4a1 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -94,7 +94,7 @@ Section borrow.
     iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". { done. }
     iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
     iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton -wp_fupd. wp_read.
-    iMod ("Hclose'" $! (l↦#l' ∗ ⎡freeable_sz n (ty_size ty) l'⎤ ∗ _)%I
+    iMod ("Hclose'" $! (_↦#l' ∗ ⎡freeable_sz n (ty_size ty) l'⎤ ∗ _)%I
           with "[] [H↦ Hown H†]") as "[Hbor Htok]"; last 1 first.
     - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". { done. }
       iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". { done. }
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 76c961af..9fab81d0 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -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 "!>" (? args) "*". 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/lib/arc.v b/theories/typing/lib/arc.v
index e04a4162..71b899d2 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -173,14 +173,14 @@ Section arc.
                 ∃ q' ts tw, shared_arc_local _ _ _ _ _ ∗ &at{_,_} _)%I).
     iMod (inv_alloc shrN _ (idx_bor_own i V ∨ C V)%I
           with "[Hpbown]") as "#Hinv"; [by iLeft; iFrame|].
-    iIntros "!> !> * % Htok".
+    iIntros "!> !>" (F q0 ?) "Htok".
     iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
       { rewrite bor_unfold_idx. iExists _. by iFrame. }
       iClear "H↦ Hinv Hpb".
       rewrite -(Qp.div_2 q0). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
-      remember ((full_arc_own _ _ _ ∨ shared_arc_own _ _ _)%I) as X.
+      remember ((full_arc_own _ _ _ ∨ shared_arc_own _ _ _)%I) as X eqn:HeqX.
       iApply (monPred_in_elim with "Hin"). iModIntro. iSpecialize ("Htok" $! V V).
       iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
       iModIntro. iNext. iAssert (shared_arc_own l' ty tid V)%I with "[>HP]" as "HX".
@@ -238,7 +238,7 @@ Section arc.
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
     iSplit; first done. iSplit; iModIntro.
-    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+    - iIntros (tid vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
       { iLeft. iFrame. iDestruct "Hsz" as %->.
         iFrame. iApply (heap_mapsto_pred_wand with "Hc"). iApply "Hoincl". }
@@ -312,7 +312,7 @@ Section arc.
                 ∃ q' ts tw, shared_arc_local _ _ _ _ _ ∗ &at{_,_} _)%I).
     iMod (inv_alloc shrN _ (idx_bor_own i V ∨ C V)%I
           with "[Hpbown]") as "#Hinv"; first by iLeft; iFrame.
-    iIntros "!> !> * % Htok".
+    iIntros "!> !>" (F q0 ?) "Htok".
     iMod (inv_acc with "Hinv") as "[INV Hclose1]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
@@ -363,7 +363,7 @@ Section arc.
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
     iSplit; first done. iSplit; iModIntro.
-    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+    - iIntros (tid vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as (???? ν ? ?) "(#Hpersist & Htk)".
       iExists _, _, _, _, _, _, _. iFrame "#∗". by iApply arc_persist_type_incl.
     - iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
@@ -922,7 +922,7 @@ Section arc.
     iDestruct "Hrc'" as (γi γs γw γsw ν t q) "[#Hpersist Htok]". wp_bind (drop_weak _).
     iApply (drop_weak_spec with "[] [Htok]");
       [|by iDestruct "Hpersist" as "[$?]"|by iExists _|]. { solve_ndisj. }
-    iIntros "!> * Hdrop". wp_bind (if: _ then _ else _)%E.
+    iIntros "!>" (b) "Hdrop". wp_bind (if: _ then _ else _)%E.
     iApply (wp_wand _ _ _ (λ _, True)%I with "[Hdrop]").
     { destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
       iDestruct "H↦" as (vl) "[? Heq]". iDestruct "Heq" as %<-.
@@ -989,7 +989,7 @@ Section arc.
       iIntros "[Hr1 Hrc']". wp_seq. wp_bind (drop_weak _).
       wp_apply (drop_fake_spec with "[//] [$Hend Hrc' H†] "); [solve_ndisj|..].
       { unfold P2. auto with iFrame. }
-      iIntros "* Hdrop". wp_bind (if: _ then _ else _)%E.
+      iIntros (b) "Hdrop". wp_bind (if: _ then _ else _)%E.
       iApply (wp_wand _ _ _ (λ _, True)%I with "[Hdrop]").
       { destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
         iDestruct "H↦" as (vl') "[? Heq]". iDestruct "Heq" as %<-.
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index 5685986d..57685235 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -89,10 +89,10 @@ Section diverging_static.
     { iIntros (k). simpl_subst.
       iApply type_equivalize_lft_static_bad.
       iApply (type_call [ϝ] ()); solve_typing. }
-    iIntros "!> *". inv_vec args=>r. simpl_subst.
+    iIntros "!>" (? args) "*". 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 "!>" (? args) "*". inv_vec args. simpl_subst.
     iApply type_jump; solve_typing.
   Qed.
 End diverging_static.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 8e9067d4..ffd35d9d 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -88,7 +88,7 @@ Section mutex.
     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 "!>" (tid vl) "Hvl". destruct vl as [|[[| |n]|]vl]; try done.
       simpl. iDestruct "Hvl" as "[$ [$ Hvl]]". by iApply "Howni".
     - iIntros "!> * Hshr". iDestruct "Hshr" as (κ') "[Hincl Hshr]".
       iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ) "Hproto".
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 67d3f232..5484fbf5 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 "!>" (??? args).
     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 7cb63f0f..61efc9bb 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -218,7 +218,7 @@ Section rc.
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
     iSplit; first done. iSplit; iModIntro.
-    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+    - iIntros (tid vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
       { iLeft. iFrame. iDestruct "Hsz" as %->.
         iFrame. iApply (heap_mapsto_pred_wand with "Hc"). iApply "Hoincl". }
@@ -593,7 +593,7 @@ Section code.
     { exfalso. destruct Hincl as [Hincl|Hincl].
       - by inversion Hincl.
       - apply csum_included in Hincl. naive_solver. }
-    iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'† & >% & Hνtok & Hν†)".
+    iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'† & >%H & Hνtok & Hν†)".
     wp_read. wp_let. wp_op. rewrite shift_loc_0. wp_op. wp_write. wp_write.
     (* And closing it again. *)
     iMod (own_update with "Hrc●") as "[Hrc● Hrctok2]".
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 2970101e..4bf178dc 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -88,7 +88,7 @@ Section weak.
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(Hsz & #Hoincl & #Hsincl)".
     iSplit; first done. iSplit; iModIntro.
-    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
+    - iIntros (tid vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as (γ ν) "(#Hpersist & Htok)".
       iExists _, _. iFrame "Htok". by iApply rc_persist_type_incl.
     - iIntros "* #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
@@ -404,7 +404,7 @@ Section code.
       iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
       iDestruct (own_valid_2 with "Hrc● Hwtok") as
           %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
-      destruct weakc; first by simpl in *; lia.
+      destruct weakc as [|weakc]; first by simpl in *; lia.
       iMod (own_update_2 with "Hrc● Hwtok") as "Hrc●".
       { apply auth_update_dealloc, prod_local_update_2,
               (cancel_local_update_unit 1%nat), _. }
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 8afd3112..82bc2875 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -75,7 +75,7 @@ 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 (tid l γ α) "!> #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".
@@ -188,10 +188,10 @@ Section refcell.
     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"].
+    iSplit; [|iSplit; iIntros "!>" (tid vl)].
     - iPureIntro. simpl. congruence.
-    - destruct vl as [|[[]|]]=>//=. by iApply "Hown".
-    - simpl. iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
+    - iIntros "H". destruct vl as [|[[]|]]=>//=. by iApply "Hown".
+    - iIntros (l) "H". simpl. iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
       iApply na_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H".
       + by iApply "Hty1ty2". + by iApply "Hty2ty1".
   Qed.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 9d3c4c8e..0e67e070 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -442,11 +442,11 @@ Section rwlock.
     iDestruct (EQ' with "HL") as "#EQ'".
     iDestruct (rwlock_proto_proper with "HL") as "#Hty1ty2"; first done.
     iIntros "!> #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
-    iSplit; [|iSplit; iIntros "!> * H"].
+    iSplit; [|iSplit; iIntros "!>" (tid vl)].
     - iPureIntro. simpl. congruence.
-    - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ [$ H]]".
+    - iIntros "H". destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ [$ H]]".
       by iApply "Hown".
-    - iDestruct "H" as (α) "[Ha H]". iExists α. iFrame "Ha".
+    - iIntros (l) "H". iDestruct "H" as (α) "[Ha H]". iExists α. iFrame "Ha".
       iDestruct "H" as (????) "lc". iExists _,_,_,_.
       by iApply ("Hty1ty2" with "HE lc").
   Qed.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index d8887092..f4e2b16a 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -31,7 +31,7 @@ Section join_handle.
     ▷ type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
   Proof.
     iIntros "#Hincl". iSplit; first done. iSplit; iModIntro.
-    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done. simpl.
+    - iIntros (tid vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done. simpl.
       iApply (join_handle_impl with "[] Hvl"). iIntros "!> * Hown" (tid').
       iDestruct (box_type_incl with "Hincl") as "{Hincl} (_ & Hincl & _)".
       iApply "Hincl". done.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 241daeef..f1796172 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -80,7 +80,7 @@ Section own.
     intros _ ty κ κ' tid l. iIntros "#Hκ #H".
     iDestruct "H" as (l') "[Hfb #Hvs]".
     iExists l'. iSplit. { by iApply (frac_bor_shorten with "[]"). }
-    iIntros "!> *% Htok".
+    iIntros "!>" (F q ?) "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.
@@ -234,7 +234,7 @@ Section typing.
     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 !>".
+    iExists _, _, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !>".
     iExists _. auto.
   Qed.
 
@@ -245,7 +245,7 @@ Section typing.
     iIntros ([[]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
     iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%".
-    iExists l, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
+    iExists _, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
     iExists _. iFrame. done.
   Qed.
 
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 0b5beabe..ad288722 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -22,11 +22,11 @@ Section product_split.
     tctx_interp tid $ hasty_ptr_offsets p ptr tyl (off1 + off2)%nat.
   Proof.
     intros Hp.
-    revert off1 off2; induction tyl; intros off1 off2; simpl; first done.
+    revert off1 off2; induction tyl as [|?? IHtyl]; intros off1 off2; simpl; first done.
     rewrite !tctx_interp_cons. f_equiv; last first.
     { by rewrite IHtyl assoc_L. }
     apply tctx_elt_interp_hasty_path. clear Hp. simpl.
-    clear. destruct (eval_path p); last done. destruct v; try done.
+    clear. destruct (eval_path p) as [v|]; last done. destruct v as [l|]; try done.
     destruct l; try done. rewrite shift_loc_assoc !Nat2Z.id //.
   Qed.
 
@@ -65,8 +65,8 @@ Section product_split.
     iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]".
     iDestruct "Hp" as %Hp. iDestruct (Hloc with "Hty") as %[l [=->]].
     assert (eval_path p = Some #l) as Hp'.
-    { move:Hp. simpl. clear. destruct (eval_path p); last done.
-      destruct v; try done. destruct l0; try done. rewrite shift_loc_0. done. }
+    { move:Hp. simpl. clear. destruct (eval_path p) as [v|]; last done.
+      destruct v as [l0|]; try done. destruct l0; try done. rewrite shift_loc_0. done. }
     clear Hp. destruct tyl.
     { assert (eqtype E L (ptr ty) (ptr (product2 ty unit))) as [Hincl _].
       { rewrite right_id. done. }
@@ -111,7 +111,7 @@ Section product_split.
     iDestruct "H1" as "(H↦1 & H†1)".
     iDestruct "H2" as (v2) "(Hp2 & H2)". simpl. iDestruct "Hp1" as %Hρ1.
     rewrite Hρ1. iDestruct "Hp2" as %[=<-]. iDestruct "H2" as "[H↦2 H†2]".
-    iExists #l. iSplitR; first done. rewrite /= -freeable_sz_split Nat2Z.id. iFrame.
+    iExists #_. iSplitR; first done. rewrite /= -freeable_sz_split Nat2Z.id. iFrame.
     iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
     iExists (vl1 ++ vl2). rewrite heap_mapsto_vec_app. iFrame.
     iDestruct (ty_size_eq with "H1") as "#>EQ". iDestruct "EQ" as %->.
@@ -158,7 +158,7 @@ Section product_split.
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]"; try done.
     iDestruct "Hp1" as %Hp1. iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1.
-    iDestruct "Hp2" as %[=<-]. iExists #l. iFrame "%".
+    iDestruct "Hp2" as %[=<-]. iExists #_. iFrame "%".
     iMod (bor_combine with "LFT H1 H2") as "H"; first solve_ndisj.
     by rewrite Nat2Z.id /= split_prod_mt.
   Qed.
@@ -207,7 +207,7 @@ Section product_split.
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 Hown1]"; try done.
     iDestruct "Hp1" as %Hp1. iDestruct "H2" as ([[]|]) "[Hp2 Hown2]"; try done.
-    rewrite /= Hp1 Nat2Z.id. iDestruct "Hp2" as %[=<-]. iExists #l. by iFrame.
+    rewrite /= Hp1 Nat2Z.id. iDestruct "Hp2" as %[=<-]. iExists _. by iFrame (Hp1) "∗".
   Qed.
 
   Lemma shr_is_ptr κ ty tid (vl : list val) :
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 400c3d22..fa26d247 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -441,7 +441,7 @@ Section type.
   Lemma shr_locsE_shift l n m :
     shr_locsE l (n + m) = shr_locsE l n ∪ shr_locsE (l +ₗ n) m.
   Proof.
-    revert l; induction n; intros l.
+    revert l; induction n as [|? IHn]; intros l.
     - rewrite shift_loc_0. set_solver+.
     - rewrite -Nat.add_1_l /= IHn shift_loc_assoc.
       set_solver+.
@@ -450,11 +450,11 @@ Section type.
   Lemma shr_locsE_disj l n m :
     shr_locsE l n ## shr_locsE (l +â‚— n) m.
   Proof.
-    revert l; induction n; intros l.
+    revert l; induction n as [|n IHn]; intros l.
     - simpl. set_solver+.
     - rewrite -Nat.add_1_l -shift_loc_assoc /=.
       apply disjoint_union_l. split; last exact : IHn.
-      clear IHn. revert n; induction m; intros n; simpl; first set_solver+.
+      clear IHn. revert n; induction m as [|? IHm]; intros n; simpl; first set_solver+.
       rewrite shift_loc_assoc. apply disjoint_union_r. split.
       + apply ndot_ne_disjoint. destruct l. intros [=]. lia.
       + move:(IHm (n + 1)%nat). by rewrite -!shift_loc_assoc.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 8ae9561d..18fe9b82 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -43,12 +43,16 @@ Section type_context.
   Proof.
     revert v; induction p; intros v; cbn -[to_val];
       try (intros <-%of_to_val; by iApply wp_value).
-    destruct op; try discriminate; [].
-    destruct p2; try (intros ?; by iApply wp_value); [].
-    destruct l; try (intros ?; by iApply wp_value); [].
-    destruct (eval_path p1); try done.
-    destruct v0; try discriminate; [].
-    destruct l; try discriminate; [].
+    match goal with H : bin_op |- _ => destruct H; try discriminate; [] end.
+    case_match; try (intros ?; by iApply wp_value); [].
+    case_match; try (intros ?; by iApply wp_value); [].
+    case_match; try done.
+    case_match; try discriminate; [].
+    case_match; try discriminate; [].
+    match goal with H : eval_path ?p = Some _ |- _ => rename p into p1 end.
+    match goal with H : (∀ _, _ -> ⊢ WP p1 @ tid; E {{ λ _, _ }}) |- _ =>
+      rename H into IHp1
+    end.
     intros [=<-]. wp_bind p1. iApply (wp_wand with "[]").
     { iApply IHp1. done. }
     iIntros (v) "%". subst v. wp_op. done.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index a01ed2c2..2a8eaeb8 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -80,7 +80,7 @@ Section case.
     wp_read. wp_case; first (split; [lia|by rewrite Nat2Z.id]).
     iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'.
     destruct Hety as [Hety|Hety].
-    - iMod ("Hclose'" $! ((l +ₗ 1) ↦∗: ty.(ty_own) tid)%I
+    - iMod ("Hclose'" $! ((_ +ₗ 1) ↦∗: ty.(ty_own) tid)%I
             with "[H↦i H↦vl''] [H↦vl' Hown]") as "[Hb Htok]".
       { iIntros "!>Hown". iDestruct "Hown" as (vl'2) "[H↦ Hown]".
         iExists (#i::vl'2++vl''). iIntros "!>". iNext.
@@ -168,7 +168,8 @@ Section case.
     iIntros (? ->). wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"); [done|].
     iIntros (v2 Hv2) "Hty2". iDestruct (ty_size_eq with "Hty2") as %Hlenty.
     destruct vl as [|? vl].
-    { exfalso. revert i Hty. clear - Hlen Hlenty. induction tyl=>//= -[|i] /=.
+    { exfalso. revert i Hty. clear - Hlen Hlenty.
+      induction tyl as [|?? IHtyl]=>//= -[|i] /=.
       - intros [= ->]. simpl in *. lia.
       - apply IHtyl. simpl in *. lia. }
     rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
@@ -249,7 +250,7 @@ Section case.
     rewrite typed_read_eq in Hr.
     iMod (Hr with "[] LFT HE Htl HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=.
     clear Hr. subst. assert (ty.(ty_size) ≤ length vl1).
-    { revert i Hty. rewrite Hlen. clear. induction tyl=>//= -[|i] /=.
+    { revert i Hty. rewrite Hlen. clear. induction tyl as [|?? IHtyl]=>//= -[|i] /=.
       - intros [= ->]. lia.
       - specialize (IHtyl i). intuition lia. }
     rewrite -(take_drop (ty.(ty_size)) vl1) heap_mapsto_vec_app.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 18032c94..d9c7adf1 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -41,7 +41,7 @@ Section uninit.
        ty_shr := (uninit0 n).(ty_shr) |}.
   Next Obligation. iIntros (???) "%". done. Qed.
   Next Obligation.
-    iIntros (???????) "LFT Hvl". iApply (ty_share (uninit0 n) with "LFT"); first done.
+    iIntros (n ??????) "LFT Hvl". iApply (ty_share (uninit0 n) with "LFT"); first done.
     iApply (bor_iff with "[] Hvl"). iIntros "!> !>". setoid_rewrite uninit0_own.
     iSplit; iIntros; done.
   Qed.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index ae61678d..027962ae 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -33,7 +33,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 "!>" (F q ?) "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 "$".
diff --git a/theories/typing/util.v b/theories/typing/util.v
index b8433379..9aed4d7d 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -35,7 +35,7 @@ Section util.
     iMod (inv_alloc shrN _ (idx_bor_own i V ∨ ty_shr ty κ tid l V)%I
           with "[Hpbown]") as "#Hinv".
     { iModIntro. eauto. }
-    iIntros "!> !> * % Htok".
+    iIntros "!> !>" (F q ?) "Htok".
     iMod (inv_acc with "Hinv") as "[INV Hclose]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - rewrite -(Qp.div_2 q).
@@ -66,7 +66,7 @@ Section util.
     iMod (inv_alloc shrN _ (idx_bor_own i V ∨ ty_shr ty κ'' tid l V)%I
           with "[Hpbown]") as "#Hinv".
     { iModIntro. auto. }
-    iIntros "!> !> * % Htok".
+    iIntros "!> !>" (F q ?) "Htok".
     iMod (inv_acc with "Hinv") as "[INV Hclose]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - rewrite -(Qp.div_2 q).
-- 
GitLab