diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index e982eb17f35565d4c991a6545538e5630f1f456e..0c9d3409bcf51bf25226e47832f77edad5253b85 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -18,7 +18,7 @@ Section atomic_bors.
   Proof. solve_proper. Qed.
   Global Instance at_bor_contractive κ : Contractive (at_bor κ N).
   Proof. solve_contractive. Qed.
-  Global Instance at_bor_proper : Proper ((⊣⊢) ==> (⊣⊢)) (at_bor κ N).
+  Global Instance at_bor_proper κ : Proper ((⊣⊢) ==> (⊣⊢)) (at_bor κ N).
   Proof. solve_proper. Qed.
 
   Lemma at_bor_iff κ P' : ▷ □ (P ↔ P') -∗ &at{κ, N} P -∗ &at{κ, N} P'.
@@ -27,7 +27,7 @@ Section atomic_bors.
     iApply (idx_bor_iff with "HPP' HP").
   Qed.
 
-  Global Instance at_bor_persistent : Persistent (&at{κ, N} P) := _.
+  Global Instance at_bor_persistent κ N P : Persistent (&at{κ, N} P) := _.
 
   Lemma bor_share E κ :
     N ## lftN → &{κ}P ={E}=∗ &at{κ, N}P.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index ca2dc5ca6f4bc9f518fba5e1e1ade8698c13613b..d023ae35ac61efd0cffdf6d0a49202bf278b2d4e 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -49,10 +49,10 @@ Section cell.
   Lemma cell_proper' E L ty1 ty2 : eqtype E L ty1 ty2 → eqtype E L (cell ty1) (cell ty2).
   Proof. eapply cell_proper. Qed.
 
-  Global Instance cell_copy :
+  Global Instance cell_copy ty :
     Copy ty → Copy (cell ty).
   Proof.
-    intros ty Hcopy. split; first by intros; simpl; unfold ty_own; apply _.
+    intros Hcopy. split; first by intros; simpl; unfold ty_own; apply _.
     iIntros (κ tid E F l q ??) "#LFT #Hshr Htl Htok". iExists 1%Qp. simpl in *.
     (* Size 0 needs a special case as we can't keep the thread-local invariant open. *)
     destruct (ty_size ty) as [|sz] eqn:Hsz; simpl in *.
@@ -73,7 +73,7 @@ Section cell.
     by iMod ("Hclose" with "Hown Htl") as "[$ $]".
   Qed.
 
-  Global Instance cell_send :
+  Global Instance cell_send ty :
     Send ty → Send (cell ty).
   Proof. by unfold cell, Send. Qed.
 End cell.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 81ad0634679d86a37fbb8c0ea2297767ac2f9ce6..30f9e0d1b05e790f7af14d4d49ef273dc87fc453 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -71,7 +71,7 @@ Section rc.
       | _ => True
       end)%I.
 
-  Global Instance rc_inv_ne ν γ l n :
+  Global Instance rc_inv_ne tid ν γ l n :
     Proper (type_dist2 n ==> dist n) (rc_inv tid ν γ l).
   Proof.
     solve_proper_core ltac:(fun _ => f_type_equiv || f_contractive || f_equiv).
@@ -86,10 +86,10 @@ Section rc.
               (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
               □ (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν]))%I.
 
-  Global Instance rc_persist_persistent : Persistent (rc_persist tid ν γ l ty).
+  Global Instance rc_persist_persistent tid ν γ l ty : Persistent (rc_persist tid ν γ l ty).
   Proof. unfold rc_persist, tc_opaque. apply _. Qed.
 
-  Global Instance rc_persist_ne ν γ l n :
+  Global Instance rc_persist_ne tid ν γ l n :
     Proper (type_dist2 n ==> dist n) (rc_persist tid ν γ l).
   Proof.
     solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index dd212d5d358ec5e88d5d54007961ec4dce8c2a73..bb8b21c58e8c600124521e7002da6dc4a62e4a9e 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -204,9 +204,9 @@ Section refcell.
     eqtype E L ty1 ty2 → eqtype E L (refcell ty1) (refcell ty2).
   Proof. eapply refcell_proper. Qed.
 
-  Global Instance refcell_send :
+  Global Instance refcell_send ty :
     Send ty → Send (refcell ty).
-  Proof. move=>????[|[[]|]]//=. Qed.
+  Proof. move=>???[|[[]|]]//=. Qed.
 End refcell.
 
 Hint Resolve refcell_mono' refcell_proper' : lrust_typing.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 75a24847e59c0d5d16f8d99106e261f551c42679..04f19c8e4782b830713a42044cd6503bcc9bf1be 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -192,14 +192,14 @@ Section rwlock.
 
   (* Apparently, we don't need to require ty to be sync,
      contrarily to Rust's implementation. *)
-  Global Instance rwlock_send :
+  Global Instance rwlock_send ty :
     Send ty → Send (rwlock ty).
-  Proof. move=>????[|[[]|]]//=??. iIntros "[$?]". by iApply send_change_tid. Qed.
+  Proof. move=>???[|[[]|]]//=??. iIntros "[$?]". by iApply send_change_tid. Qed.
 
-  Global Instance rwlock_sync :
+  Global Instance rwlock_sync ty :
     Send ty → Sync ty → Sync (rwlock ty).
   Proof.
-    move=>???????/=. do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r.
+    move=>??????/=. do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r.
     iApply at_bor_iff. iIntros "!> !#". iApply bi.equiv_iff.
     apply bi.exist_proper=>?; do 7 f_equiv; first do 7 f_equiv.
     - do 5 f_equiv. apply bi.equiv_spec; split; iApply send_change_tid.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 0d9bff1f825bdc43683159d655301ec68f3f86a0..bcc034cbf9444c81c6543d1ed3cd45c9af09de1e 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -274,7 +274,7 @@ Section type_dist2.
       (∀ κ tid l, ty1.(ty_shr) κ tid l ≡{n}≡ ty2.(ty_shr) κ tid l) →
       type_dist2 n ty1 ty2.
 
-  Global Instance type_dist2_equivalence : Equivalence (type_dist2 n).
+  Global Instance type_dist2_equivalence n : Equivalence (type_dist2 n).
   Proof.
     constructor.
     - by constructor.