diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 5b29880c0848286e32264edde9a1f6cfc417959b..b8ea167eb375076b688cdaad86f112e9d12dc005 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -279,10 +279,10 @@ Global Instance cmra_op_ne' : NonExpansive2 (@op A _).
 Proof. intros n x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.
 Global Instance cmra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
 Proof. apply (ne_proper_2 _). Qed.
-Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
+Global Instance cmra_validN_ne' n : Proper (dist n ==> iff) (@validN A _ n) | 1.
 Proof. by split; apply cmra_validN_ne. Qed.
-Global Instance cmra_validN_proper : Proper ((≡) ==> iff) (@validN A _ n) | 1.
-Proof. by intros n x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.
+Global Instance cmra_validN_proper n : Proper ((≡) ==> iff) (@validN A _ n) | 1.
+Proof. by intros x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.
 
 Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (@valid A _).
 Proof.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 2f5974324acf63c88a1b48a558ea9794f4792aeb..b24b615059434fed786e3dd1db20d53d73a3f1ae 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -276,7 +276,7 @@ Implicit Types m : gmap K A.
 Implicit Types i : K.
 Implicit Types x y : A.
 
-Global Instance lookup_op_homomorphism :
+Global Instance lookup_op_homomorphism i :
   MonoidHomomorphism op op (≡) (lookup i : gmap K A → option A).
 Proof. split; [split|]; try apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
 
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index abe12c6cf741da058db9b4268c2c98530b101457..36a6ea4ede9a145071d75904f9f99e14a4a4f2bc 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -306,7 +306,7 @@ Section lemmas.
   Qed.
 
   (** Typeclass instances *)
-  Global Instance gmap_view_frag_core_id k v : CoreId dq → CoreId (gmap_view_frag k dq v).
+  Global Instance gmap_view_frag_core_id k dq v : CoreId dq → CoreId (gmap_view_frag k dq v).
   Proof. apply _. Qed.
 
   Global Instance gmap_view_cmra_discrete : OfeDiscrete V → CmraDiscrete (gmap_viewR K V).
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index e8b9af03465faf0ccdd24c08b7c3f829bc2192f4..d4a6f9067070b3db4151aa4f2a9c5b03fb714555 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -17,8 +17,8 @@ Global Instance cons_ne : NonExpansive2 (@cons A) := _.
 Global Instance app_ne : NonExpansive2 (@app A) := _.
 Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _.
 Global Instance tail_ne : NonExpansive (@tail A) := _.
-Global Instance take_ne : NonExpansive (@take A n) := _.
-Global Instance drop_ne : NonExpansive (@drop A n) := _.
+Global Instance take_ne n : NonExpansive (@take A n) := _.
+Global Instance drop_ne n : NonExpansive (@drop A n) := _.
 Global Instance head_ne : NonExpansive (head (A:=A)).
 Proof. destruct 1; by constructor. Qed.
 Global Instance list_lookup_ne i : NonExpansive (lookup (M:=list A) i).
@@ -37,7 +37,7 @@ Proof. intros ????; by apply Forall2_option_list, dist_option_Forall2. Qed.
 Global Instance list_filter_ne n P `{∀ x, Decision (P x)} :
   Proper (dist n ==> iff) P →
   Proper (dist n ==> dist n) (filter (B:=list A) P) := _.
-Global Instance replicate_ne : NonExpansive (@replicate A n) := _.
+Global Instance replicate_ne n : NonExpansive (@replicate A n) := _.
 Global Instance reverse_ne : NonExpansive (@reverse A) := _.
 Global Instance last_ne : NonExpansive (@last A).
 Proof. intros ????; by apply dist_option_Forall2, Forall2_last. Qed.
@@ -122,7 +122,7 @@ Instance list_bind_ne {A B : ofeT} (f : A → list A) n :
 Proof. induction 2; simpl; [constructor|solve_proper]. Qed.
 Instance list_join_ne {A : ofeT} : NonExpansive (mjoin (M:=list) (A:=A)).
 Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
-Instance zip_with_ne {A B C : ofeT} (f : A → B → C) :
+Instance zip_with_ne {A B C : ofeT} (f : A → B → C) n :
   Proper (dist n ==> dist n ==> dist n) f →
   Proper (dist n ==> dist n ==> dist n) (zip_with f).
 Proof. induction 2; destruct 1; simpl; [constructor..|f_equiv; [f_equiv|]; auto]. Qed.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 5886405b9b5ae4eb7744a60370c4fcfea3a6483b..55c1b3af1f2d0dcdd681a1af0154766eba8c3b4d 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -822,8 +822,8 @@ Section sum.
   Instance sum_dist : Dist (A + B) := λ n, sum_relation (dist n) (dist n).
   Global Instance inl_ne : NonExpansive (@inl A B) := _.
   Global Instance inr_ne : NonExpansive (@inr A B) := _.
-  Global Instance inl_ne_inj : Inj (dist n) (dist n) (@inl A B) := _.
-  Global Instance inr_ne_inj : Inj (dist n) (dist n) (@inr A B) := _.
+  Global Instance inl_ne_inj n : Inj (dist n) (dist n) (@inl A B) := _.
+  Global Instance inr_ne_inj n : Inj (dist n) (dist n) (@inr A B) := _.
 
   Definition sum_ofe_mixin : OfeMixin (A + B).
   Proof.
@@ -1003,7 +1003,7 @@ Section option.
   Proof. by constructor. Qed.
   Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
   Proof. destruct 1; split; eauto. Qed.
-  Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
+  Global Instance Some_dist_inj n : Inj (dist n) (dist n) (@Some A).
   Proof. by inversion_clear 1. Qed.
   Global Instance from_option_ne {B} (R : relation B) (f : A → B) n :
     Proper (dist n ==> R) f → Proper (R ==> dist n ==> R) (from_option f).
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index fb6601ad17a05177ceda026a7058bc4615af5f79..e600610dee00db9f1b2b7ef343c5238bd9ca5331 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -313,7 +313,7 @@ Qed.
 Section big_op_instances.
   Context `{!inG Σ (A:ucmraT)}.
 
-  Global Instance own_cmra_sep_homomorphism :
+  Global Instance own_cmra_sep_homomorphism γ :
     WeakMonoidHomomorphism op uPred_sep (≡) (own γ).
   Proof. split; try apply _. apply own_op. Qed.
 
@@ -334,7 +334,7 @@ Section big_op_instances.
     own γ ([^op mset] x ∈ X, g x) ⊣⊢ [∗ mset] x ∈ X, own γ (g x).
   Proof. apply (big_opMS_commute1 _). Qed.
 
-  Global Instance own_cmra_sep_entails_homomorphism :
+  Global Instance own_cmra_sep_entails_homomorphism γ :
     MonoidHomomorphism op uPred_sep (⊢) (own γ).
   Proof.
     split; [split|]; try apply _.
diff --git a/theories/proofmode/class_instances_later.v b/theories/proofmode/class_instances_later.v
index 1f850ff695d125d8c235ac5bf4c5e0fba3486e56..ffab7068c7775a9012011705441a422f8b652f5c 100644
--- a/theories/proofmode/class_instances_later.v
+++ b/theories/proofmode/class_instances_later.v
@@ -235,7 +235,7 @@ Global Instance into_except_0_persistently P Q :
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
 
 (** ElimModal *)
-Global Instance elim_modal_timeless p P Q :
+Global Instance elim_modal_timeless p P P' Q :
   IntoExcept0 P P' → IsExcept0 Q → ElimModal True p p P P' Q Q.
 Proof.
   intros. rewrite /ElimModal (except_0_intro (_ -∗ _)%I) (into_except_0 P).
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 6d4a660ed5eddbca2ed38af982b8677bc4b6cc63..2dbbfd3a4e6f3918d04605262d8fd0ecd5ececa8 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -312,7 +312,7 @@ Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
 Global Instance make_laterN_emp `{!BiAffine PROP} n :
   @KnownMakeLaterN PROP n emp emp | 0.
 Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
-Global Instance make_laterN_default P : MakeLaterN n P (â–·^n P) | 100.
+Global Instance make_laterN_default n P : MakeLaterN n P (â–·^n P) | 100.
 Proof. by rewrite /MakeLaterN. Qed.
 
 Global Instance frame_later p R R' P Q Q' :
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 93983d9d9117b21ba6433ebb1faf8b1960c15102..e9012f26876348a470bc834fde5e439fa9534d96 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -158,16 +158,14 @@ Proof.
   apply  bi.intuitionistically_if_elim.
 Qed.
 
-Global Instance from_assumption_make_monPred_objectively P Q :
+Global Instance from_assumption_make_monPred_objectively p P Q :
   FromAssumption p P Q → KnownLFromAssumption p (<obj> P) Q.
 Proof.
-  intros ?.
   by rewrite /KnownLFromAssumption /FromAssumption monPred_objectively_elim.
 Qed.
-Global Instance from_assumption_make_monPred_subjectively P Q :
+Global Instance from_assumption_make_monPred_subjectively p P Q :
   FromAssumption p P Q → KnownRFromAssumption p P (<subj> Q).
 Proof.
-  intros ?.
   by rewrite /KnownRFromAssumption /FromAssumption -monPred_subjectively_intro.
 Qed.