diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 8b400fd551a8937d4d89a970e42ea103eee72c0c..734a2dbf699470beef0b0f11ba37e1b5d8cba5d1 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -398,7 +398,7 @@ Section arc.
     { 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 _.
+      destruct st' as [[[[q' c]?]| |]|]; try done; iExists _.
       - iDestruct "H" as (q) "(>Heq & [HP1 HP1'] & >$ & ?)". iDestruct "Heq" as %Heq.
         iIntros "!>"; iSplit; iMod ("Hclose2" with "Hown") as "HP".
         + iIntros "_ Hl". iExists (q/2)%Qp. iMod (own_update with "H●") as "[H● $]".
@@ -408,7 +408,7 @@ Section arc.
             apply frac_valid. rewrite /= -Heq comm_L.
             by apply Qp_add_le_mono_l, Qp_div_le. }
           iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
-          rewrite /= [xH â‹… _]comm_L frac_op [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
+          rewrite /= [xH â‹… _]comm_L frac_op [(_ + q')%Qp]comm -[(_ + _)%Qp]assoc
                   Qp_div_2 left_id_L. auto with iFrame.
         + iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
           iExists q. auto with iFrame.
@@ -597,7 +597,7 @@ Section arc.
         iInv N as ([st w]) "[>H● H]" "Hclose".
         iDestruct (own_valid_2 with "H● H◯") as
            %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
-        simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & Hincl); last first.
+        simpl in Hincl. destruct Hincl as (x1 & x2 & [=<-] & -> & Hincl); last first.
         assert (∃ q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->).
         { destruct Hincl as [|Hincl]; first by setoid_subst; eauto.
           apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index 3e049e4463d6ec317bd24c3093d77b1c28baaf9a..7f70f113f48ba63dee00b3d98828a8860050ccbe 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -24,7 +24,7 @@ Section specs.
     iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
     - wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
       rewrite heap_mapsto_vec_nil. auto.
-    - wp_if. wp_alloc l as "H↦" "H†". lia. iApply "HΦ". subst sz. iFrame.
+    - wp_if. wp_alloc l as "H↦" "H†". lia. iApply "HΦ". subst. iFrame.
   Qed.
 
   Lemma wp_delete E (n:Z) l vl :
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index ba10d822749bf0cdf5c859f1fd3d5fa17af104f7..44f7f1cb67c3f4d61905c020ca19ad5cd8994310 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -351,7 +351,7 @@ Proof.
     change (App (of_val vf) ((of_val <$> vs) ++ e :: el)) with (fill_item (AppRCtx vf vs el) e).
     iApply wp_bind. iApply (wp_wand with "He"). iIntros (v) "HQ /=".
     rewrite cons_middle (assoc app) -(fmap_app _ _ [v]).
-    iApply (IH _ _ with "Hl"). iIntros "* Hvl". rewrite -assoc.
+    iApply (IH _ _ with "Hl"). iIntros "%vl Hvl". rewrite -assoc.
     iApply ("HΦ" $! (v:::vl)). iFrame.
 Qed.
 
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 2f7a11b40ffeabe024b730994bfaa25ce6a9ae28..1988a5ea9d3405b184b9b05fe1680d05997e2502 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -90,7 +90,7 @@ Section borrow.
     rewrite tctx_interp_singleton.
     iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
-    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
+    wp_apply (wp_hasty with "Hp"). iIntros ([[|l|]|]) "_ Hown"; try done.
     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.
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 617eed75f5b8bde8dbc18a2165fbf2c071dc4f36..1592cc1960fdfd7665469b5e1f5ba744931ebea5 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 "!> %k %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 ff2a94ade604006a7007b3249346723629f52456..c49af0d5e7eaa56b1d1173b195095371b90e535d 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -178,13 +178,13 @@ 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". }
       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 "%κ %tid %l #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
       iIntros "{$Hfrac} !> * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
       iModIntro. iNext. iMod "H" as "[$ H]".
       iDestruct "H" as (γ ν q') "(Hlft & Hpersist & Hna)".
@@ -291,10 +291,10 @@ 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'.
+    - iIntros "%κ %tid %l #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
       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.
@@ -818,7 +818,7 @@ Section arc.
     rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
     iDestruct "Hrc'" as (γ ν) "[#Hpersist Htok]". wp_bind (drop_weak _).
     iApply (drop_weak_spec with "[] [Htok]"); [by iDestruct "Hpersist" as "[$?]"|by auto|].
-    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 %<-.
@@ -882,7 +882,7 @@ Section arc.
       iIntros "[Hr1 Hrc']". wp_seq. wp_bind (drop_weak _).
       iMod ("Hend" with "[$H† Hrc']") as "Htok"; first by eauto.
       iApply (drop_weak_spec with "Ha Htok").
-      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 6ca1456e56c87f68ba66a6e924dbc60db9aa2cf6..d0a14ca188379c94446c62cf160d5f5d22ba32ac 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 "!> %k %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 "!> %k' %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 95bb5d5ff516908ace33feec318d5125a495a141..f87a146757a07b774f660de18d2e3a4984a94add 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -94,9 +94,9 @@ 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]".
+    - iIntros "!> %κ %tid %l 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.
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index c3155163ecafe88e48b3baa5a4b2044bf967904c..28b7991da6ea40293ee0587154d7b6a71e90fc6a 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 "!> _ %κ %ret %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 ae5bb6077951a0ca586c524b97f138bd52bf144e..e2c0374c0e73031e90cef924a513cc3bbd9ed5f9 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -211,13 +211,13 @@ 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". }
       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 "%κ %tid %l #Hshr". iDestruct "Hshr" as (l') "[Hfrac Hshr]". iExists l'.
       iIntros "{$Hfrac} !> * % Htok". iMod ("Hshr" with "[% //] Htok") as "{Hshr} H".
       iModIntro. iNext. iMod "H" as "[$ H]".
       iDestruct "H" as (γ ν q') "(Hlft & Hpersist & Hna)".
@@ -584,13 +584,13 @@ Section code.
     setoid_subst; try done; last first.
     { 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'† & >%Hq & 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]".
     { apply auth_update_alloc, prod_local_update_1,
       (op_local_update_discrete _ _ (Some (Cinl ((qb/2)%Qp, 1%positive))))=>-[/= Hqa _].
-      split; simpl; last done. apply frac_valid. rewrite /= -H comm_L.
+      split; simpl; last done. apply frac_valid. rewrite /= -Hq comm_L.
       by apply Qp_add_le_mono_l, Qp_div_le. }
     rewrite right_id -Some_op -Cinl_op -pair_op. iDestruct "Hνtok" as "[Hνtok1 Hνtok2]".
     iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 5e309dbcb32b39d6a0a6abab226143ebcfc5f9ac..b87dbc9dccee1f56e368dadddd78829fd50f88fb 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -76,7 +76,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,11 @@ 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; last iSplit.
     - iPureIntro. simpl. congruence.
-    - destruct vl as [|[[]|]]=>//=. by iApply "Hown".
-    - simpl. iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
+    - iIntros "!> %tid %vl H". destruct vl as [|[[]|]]=>//=. by iApply "Hown".
+    - iIntros "!> %α %tid %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 fc2380eafd19896d338b79da0a4a601d9f6bd2ad..7caefcf07605fc979855bfe9fc34ef532d4c3baa 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -69,7 +69,7 @@ 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 "%tid_own %tid_shr %l %γ %α !> #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".
@@ -195,10 +195,12 @@ Section rwlock.
     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"].
+    iSplit; [|iSplit].
     - iPureIntro. simpl. congruence.
-    - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
-    - iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
+    - iIntros "!> %tid %vl H". destruct vl as [|[[]|]]; try done.
+      iDestruct "H" as "[$ H]". by iApply "Hown".
+    - iIntros "!> %α %tid %l H". simpl.
+      iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
       iApply at_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H".
       by iApply "Hty1ty2". by iApply "Hty2ty1".
   Qed.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 85344026990854daa9dd325b2327cbcd6f4966c5..c3e953d2d9e32c61ede85ff2082adf98792942d4 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -270,8 +270,8 @@ Section rwlock_functions.
     iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". done.
     wp_bind (CAS _ _ _).
     iMod (at_bor_acc_tok with "LFT Hinv Hβtok") as "[INV Hclose'']"; try done.
-    iDestruct "INV" as (st) "(Hlx & >Hownst & Hst)". destruct st.
-    - iApply (wp_cas_int_fail with "Hlx"). by destruct c as [|[[]]|].
+    iDestruct "INV" as (st) "(Hlx & >Hownst & Hst)". destruct st as [c|].
+    - iApply (wp_cas_int_fail with "Hlx"); first by destruct c as [|[[]]|].
       iNext. iIntros "Hlx".
       iMod ("Hclose''" with "[Hlx Hownst Hst]") as "Hβtok"; first by iExists _; iFrame.
       iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index c8b96eb3a05a5423c430e8de6a94dc03b3dc8e20..b51fbaf521f580ae4187674cf891bbb9c6e00436 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.
+    - iIntros "%tid %vl Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       simpl. iApply (join_handle_impl with "[] Hvl"). clear tid.
       iIntros "!> * Hown" (tid).
       iDestruct (box_type_incl with "Hincl") as "{Hincl} (_ & Hincl & _)".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 822223da2bddb59138a3d18a20c0b748ddd512aa..af3db712e365878eabfcc8070ec477208a0f391a 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 "!> %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.
@@ -230,7 +230,7 @@ Section typing.
     Copy ty → ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n ty).
   Proof.
     rewrite typed_read_eq. iIntros (Hsz) "!>".
-    iIntros ([[]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
+    iIntros ([[|l|]|] 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 _. auto.
@@ -240,7 +240,7 @@ Section typing.
     ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
   Proof.
     rewrite typed_read_eq. iModIntro.
-    iIntros ([[]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
+    iIntros ([[|l|]|] 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 !> !>".
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 706012283b147e4e99d0e19bbeb0388c61784aec..0563f6a059e610d1160aeb9ba2088a86c2ce8310 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 [|ty tyl IH]; intros off1 off2; simpl; first done.
     rewrite !tctx_interp_cons. f_equiv; last first.
-    { by rewrite IHtyl assoc_L. }
+    { by rewrite IH 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.inj_add //.
   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 [l'|]; try done. destruct l'; 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. }
@@ -107,7 +107,7 @@ Section product_split.
   Proof.
     iIntros (tid qmax qL) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
-    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "(Hp1 & H1)"; try done.
+    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[|l|]|]) "(Hp1 & H1)"; try done.
     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]".
@@ -156,7 +156,7 @@ Section product_split.
   Proof.
     iIntros (tid qmax qL) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
-    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]"; try done.
+    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[|l|]|]) "[Hp1 H1]"; try done.
     iDestruct "Hp1" as %Hp1. iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1.
     iDestruct "Hp2" as %[=<-]. iExists #l. iFrame "%".
     iMod (bor_combine with "LFT H1 H2") as "H"; first solve_ndisj. by rewrite /= split_prod_mt.
@@ -204,7 +204,7 @@ Section product_split.
   Proof.
     iIntros (tid qmax qL) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
-    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 Hown1]"; try done.
+    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[|l|]|]) "[Hp1 Hown1]"; try done.
     iDestruct "Hp1" as %Hp1. iDestruct "H2" as ([[]|]) "[Hp2 Hown2]"; try done.
     rewrite /= Hp1. iDestruct "Hp2" as %[=<-]. iExists #l. by iFrame.
   Qed.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 33339544c15b4df6563ed163844af1957d1e904b..ea40b66fbbd318c3c2f943d6f7dfeb1661fd80e2 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -435,7 +435,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 [|n IHn]; intros l.
     - rewrite shift_loc_0. set_solver+.
     - rewrite -Nat.add_1_l Nat2Z.inj_add /= IHn shift_loc_assoc.
       set_solver+.
@@ -444,11 +444,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 Nat2Z.inj_add /=.
       apply disjoint_union_l. split; last (rewrite -shift_loc_assoc; exact: IHn).
-      clear IHn. revert n; induction m; intros n; simpl; first set_solver+.
+      clear IHn. revert n; induction m as [|m IHm]; intros n; simpl; first set_solver+.
       rewrite shift_loc_assoc. apply disjoint_union_r. split.
       + apply ndot_ne_disjoint. destruct l. intros [=]. lia.
       + rewrite -Z.add_assoc. move:(IHm (n + 1)%nat). rewrite Nat2Z.inj_add //.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 01e52295213fd30e28d0d6637fefee7724b02cc5..2f9fe91769ba1b6471f6aef5c1e3d9527ff1739d 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -41,14 +41,17 @@ Section type_context.
     revert v; induction p; intros v; try done.
     { intros [=]. by iApply wp_value. }
     { move=> /of_to_val=> ?. by iApply wp_value. }
-    simpl. 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; [].
-    intros [=<-]. wp_bind p1. iApply (wp_wand with "[]").
-    { iApply IHp1. done. }
+    simpl.
+    case_match; try discriminate; [].
+    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; [].
+    intros [=<-].
+    match goal with |- context[(?l +â‚— _)%E] => rename l into p1 end.
+    wp_bind p1. iApply (wp_wand with "[]").
+    { match goal with H: context[(WP p1 @ _ {{ _, _ }})%I] |- _ => iApply H end. done. }
     iIntros (v) "%". subst v. wp_op. done.
   Qed.
 
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 4d2212e5eb7d9a971154fe9cbb9ac2cbc9521be7..1084b37df630f0a992da5689f2ddf40ad3575aaf 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -65,7 +65,7 @@ Section case.
   Proof.
     iIntros (Halive Hel tid qmax) "#LFT #HE Hna HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
-    iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
+    iApply (wp_hasty with "Hp"). iIntros ([[|l|]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
     iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
     iMod (bor_acc_cons with "LFT Hp Htok") as "[H↦ Hclose']". done.
@@ -167,9 +167,10 @@ Section case.
     iIntros (? ->). wp_op. wp_bind p2. iApply (wp_hasty with "Hp2").
     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 [|ty' tyl IH]=>//= -[|i] /=.
       - intros [= ->]. simpl in *. lia.
-      - apply IHtyl. simpl in *. lia. }
+      - apply IH. simpl in *. lia. }
     rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦vl" as "[H↦ H↦vl]". wp_write.
     rewrite tctx_interp_singleton tctx_hasty_val' //.
     iMod ("Hw" with "[-HLclose]") as "[HL $]"; last first.
@@ -248,9 +249,10 @@ 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 [|ty' tyl IH]=>//= -[|i] /=.
       - intros [= ->]. lia.
-      - specialize (IHtyl i). intuition lia. }
+      - specialize (IH i). intuition lia. }
     rewrite -(take_drop (ty.(ty_size)) vl1) heap_mapsto_vec_app.
     iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
     iDestruct (ty_size_eq with "Hty") as "#>%".
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index ee81c610f2c244f007b60ab70845885896c12cb7..4b2c877e323293e059fd6c37216ffc76d5eba1ed 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 113f50ea29cd06b243d043a81285797cd04df4fa..9fe721a8cf854d9cfe2bfc7189887ed47614f5c3 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 "!> %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 "$".