diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index a085a0179fd13466f8af703fb0114cb8e64f388b..d6074309f10c038a965f8e04de89b3c0ba521698 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -240,9 +240,9 @@ Section ArcInv.
     (∃ Dts, StrDowns γsw 1%Qp Dts ∗ SeenActs γw (l >> 1) Dts) ∗
     StrWkTok γsw 1%Qp)%I.
 
-  Global Instance strong_arc_timeless: Timeless (strong_arc t q l γi γs γw γsw) := _.
-  Global Instance weak_arc_timeless: Timeless (weak_arc t q l γi γs γw γsw) := _.
-  Global Instance fake_arc_timeless: Timeless (fake_arc l γi γs γw γsw) := _.
+  Global Instance strong_arc_timelesst t q l γi γs γw γsw : Timeless (strong_arc t q l γi γs γw γsw) := _.
+  Global Instance weak_arc_timeless t q l γi γs γw γsw : Timeless (weak_arc t q l γi γs γw γsw) := _.
+  Global Instance fake_arc_timeless l γi γs γw γsw : Timeless (fake_arc l γi γs γw γsw) := _.
 
   Definition strong_arc_acc l t γi γs γw γsw P E : vProp :=
     (□ (P ={E,↑histN}=∗ ∃ Vb q,
@@ -263,7 +263,7 @@ Section ArcInv.
   Definition is_arc γi γs γw γsw l : vProp :=
     view_inv γi N (arc_inv γi γs γw γsw l).
 
-  Global Instance is_arc_persistent : Persistent (is_arc γi γs γw γsw l) := _.
+  Global Instance is_arc_persistent γi γs γw γsw l : Persistent (is_arc γi γs γw γsw l) := _.
 
 End ArcInv.
 
@@ -324,10 +324,10 @@ Section arc.
     by apply view_inv_proper, arc_inv_proper.
   Qed.
 
-  Instance strong_interp_read_persistent :
+  Instance strong_interp_read_persistent γi γw γsw l γs t s v :
     Persistent (strong_interp P1 (l >> 1) γi γw γsw false l γs t s v).
-  Proof. intros. apply bi.exist_persistent. intros [[? []]|]; simpl; by apply _. Qed.
-  Instance weak_interp_read_persistent :
+  Proof. apply bi.exist_persistent. intros [[? []]|]; simpl; by apply _. Qed.
+  Instance weak_interp_read_persistent i γs γsw l γw t s v :
     Persistent (weak_interp P2 l i γs γsw false (l >> 1) γw t s v).
   Proof.
     intros. apply bi.exist_persistent.
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index d0bf4d770afe66562c89faa087fd196e2337cca6..bc049b54a374a8cb3f043c3a75c7efc1158079d7 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -20,9 +20,9 @@ Section atomic_bors.
   Proof. solve_proper. Qed.
   Global Instance at_bor_contractive κ N : Contractive (at_bor κ N).
   Proof. solve_contractive. Qed.
-  Global Instance at_bor_proper N : Proper ((≡) ==> (≡)) (at_bor κ N).
+  Global Instance at_bor_proper κ N : Proper ((≡) ==> (≡)) (at_bor κ N).
   Proof. solve_proper. Qed.
-  Global Instance at_bor_persistent N P : Persistent (&at{κ, N}P) := _.
+  Global Instance at_bor_persistent κ N P : Persistent (&at{κ, N}P) := _.
 
   Lemma at_bor_iff N P P' κ :
     ▷ □ (P ↔ P') -∗ &at{κ, N}P -∗ &at{κ, N}P'.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index ee6fbc8599ddd2dc4e321dbae362443accb4b38f..37b4fd6ce5183c57b9722bc556a385f512bfb643 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -68,7 +68,7 @@ Definition lftPreG' := lftPreG.
 Definition lftΣ Lat : gFunctors :=
   #[ boxΣ Lat; GFunctor (authR (alftUR Lat)); GFunctor (authR ilftUR);
      GFunctor (authR (borUR Lat)); GFunctor (authR natUR);  GFunctor (authR inhUR) ].
-Instance subG_lftPreG :
+Instance subG_lftPreG Lat Σ :
   subG (lftΣ Lat) Σ → lftPreG Lat Σ.
 Proof. solve_inG. Qed.
 
diff --git a/theories/lifetime/model/in_at_borrow.v b/theories/lifetime/model/in_at_borrow.v
index 6ab3a989bdfc0ac4e0af7dc70604b6d109f08838..a32326e88ab5d5c53b195312de3ab93de5bd57ed 100644
--- a/theories/lifetime/model/in_at_borrow.v
+++ b/theories/lifetime/model/in_at_borrow.v
@@ -30,9 +30,9 @@ Global Instance in_at_bor_ne κ n : Proper (dist n ==> dist n) (in_at_bor κ).
 Proof. solve_proper. Qed.
 Global Instance in_at_bor_contractive κ : Contractive (in_at_bor κ).
 Proof. solve_contractive. Qed.
-Global Instance in_at_bor_proper : Proper ((≡) ==> (≡)) (in_at_bor κ).
+Global Instance in_at_bor_proper κ : Proper ((≡) ==> (≡)) (in_at_bor κ).
 Proof. solve_proper. Qed.
-Global Instance in_at_bor_persistent : Persistent (&in_at{κ}P) := _.
+Global Instance in_at_bor_persistent κ P : Persistent (&in_at{κ}P) := _.
 
 Lemma in_at_bor_iff κ P P' :
   ▷ □ (P ↔ P') -∗ &in_at{κ}P -∗ &in_at{κ}P'.
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index 68c5d13a88060aea00f9c8f6fd7fc662d7856953..1408ae0b4625b47044b103ff8b50f5f2b0bb0bcf 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -244,7 +244,7 @@ Definition GPS_aPP IP l κ t s v γ : vProp :=
 
 Global Instance GPS_aPP_ne l κ t s v γ: NonExpansive (λ IP, GPS_aPP IP l κ t s v γ).
 Proof. move => ????. apply bi.sep_ne; [done|]. by apply at_bor_ne, GPS_PPInv_ne. Qed.
-Global Instance GPS_aPP_ne_persistent: Persistent (GPS_aPP IP l κ t s v γ) := _.
+Global Instance GPS_aPP_ne_persistent IP l κ t s v γ : Persistent (GPS_aPP IP l κ t s v γ) := _.
 
 Lemma GPS_aPP_lft_mono IP l κ κ' t s v γ :
   κ' ⊑ κ -∗ GPS_aPP IP l κ t s v γ -∗ GPS_aPP IP l κ' t s v γ.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 663e1e214844559b57a18b7c74620a7d4e1048d5..b17b655cc1ada19fd4d0a6cc9ed206d0ec710422 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -46,7 +46,7 @@ Section arc.
                                      f_type_equiv || f_contractive || f_equiv).
   Qed.
 
-  Global Instance arc_persist_persistent:
+  Global Instance arc_persist_persistent tid ν γi γs γw γsw l ty :
     Persistent (arc_persist tid ν γi γs γw γsw l ty) := _.
 
   Lemma arc_persist_type_incl tid ν γi γs γw γsw l ty1 ty2:
@@ -72,7 +72,7 @@ Section arc.
 
   Definition shared_arc_local l γs γw ts tw :=
     (∃ vs vw, GPS_SWReader l ts () vs γs ∗ GPS_SWReader (l +ₗ 1) tw () vw γw)%I.
-  Global Instance shared_arc_local_persistent :
+  Global Instance shared_arc_local_persistent l γs γw ts tw :
     Persistent (shared_arc_local l γs γw ts tw) := _.
   Lemma strong_shared_arc_local t q l γi γs γw γsw:
     strong_arc t q l γi γs γw γsw -∗ ∃ tw, shared_arc_local l γs γw t tw.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 263bd1faa6868be6fe832da01489c8272011a5ad..7848c9620a54b82999352049f9f3d8862da38aa1 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 86e8e3cc62f5049f2cfd2d649c37b8cd46ee2440..480be65c73ba942e65f0de32e86e7cbf133da34a 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -73,7 +73,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).
@@ -88,10 +88,10 @@ Section rc.
               (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
               □ (1.[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ [†ν]))%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 9885374161d181da3ceac86f1dcf1dcd206dc4e5..76b1c4087766bad9bfc4a595ef6c1a02919d37c9 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -203,9 +203,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 d2cf24200e74cfafb3c5f5dc99c2a954235b9959..9976bcfceda4cdc014a502ab210328560dc1598c 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -206,7 +206,7 @@ Section rwlock_inv.
       iExists _; iPureIntro ;(split; [done|by constructor]).
   Qed.
 
-  Global Instance rwlock_proto_persistent:
+  Global Instance rwlock_proto_persistent l γ γs κ tyO tyS tid ty :
     Persistent (rwlock_proto l γ γs κ tyO tyS tid ty) := _.
 
   Global Instance rwlock_proto_type_ne n l γ γs κ tyO tyS tid :
@@ -445,14 +445,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=>???????/=. apply bi.exist_mono=>?. apply bi.sep_mono_r.
+    move=>??????/=. apply bi.exist_mono=>?. apply bi.sep_mono_r.
     do 4 apply bi.exist_mono=>?.
     apply bi.sep_mono; last apply bi.sep_mono_l;
       apply bi.later_mono; iIntros "#H !#".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index b36995654305cf3b24e7b866d68d59f4d93a4e07..f81e2802f08a49d056e049c9e0ed3ff7a3516193 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -277,7 +277,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.