diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index db535df5d922120533bed73d5c757cf1c05f3df9..258e41ff52d48a9ac0fe8677157dbd972e67d4a2 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -316,7 +316,7 @@ Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
   `{!Contractive f} : A := compl (fixpoint_chain f).
 Definition fixpoint_aux : seal (@fixpoint_def). Proof. by eexists. Qed.
 Definition fixpoint := fixpoint_aux.(unseal).
-Arguments fixpoint {A AC AiH} f {Hf} : rename.
+Arguments fixpoint {A _ _} f {_}.
 Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
 
 Section fixpoint.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index aea6c15e00be918a9ba0e3ed9f7d54ba88caa5d8..efe8eb9b2059770cfc69852d98f83ec8cbbb5756 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -124,7 +124,7 @@ Section definitions.
   Definition meta := meta_aux.(unseal).
   Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
 End definitions.
-Arguments meta {_ _ _ _ Σ _ _ _ _} l N x.
+Arguments meta {L _ _ V Σ _ A _ _} l N x.
 
 Local Notation "l ↦{ q } v" := (mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index c95573a02ba29df72dbc5c565f709f718714c6ba..4ddbe68958da21bc8cc39ce7f8fdd54b731cfcb6 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -11,7 +11,7 @@ Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
   □ ∀ E, ⌜↑N ⊆ E⌝ → |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True).
 Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
 Definition inv := inv_aux.(unseal).
-Arguments inv {Σ i} : rename.
+Arguments inv {Σ _} N P.
 Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
 Instance: Params (@inv) 3 := {}.
 
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 79d83df864b745090c89eea6426d42eb523eea80..ed77ef6f19e44e81add28bea10c5f2a00aff89a2 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -59,7 +59,7 @@ Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
   uPred_ownM (iRes_singleton γ a).
 Definition own_aux : seal (@own_def). Proof. by eexists. Qed.
 Definition own := own_aux.(unseal).
-Arguments own {Σ A i} : rename.
+Arguments own {Σ A _} γ a.
 Definition own_eq : @own = @own_def := own_aux.(seal_eq).
 Instance: Params (@own) 4 := {}.
 
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 1be6f6992f137567a70f6fa6389ac32384e7e104..194e1ec6fe89d790cb62cc749c3903b2f231dabd 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -269,7 +269,7 @@ Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
 Definition envs_entails_eq :
   @envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
 Proof. by rewrite /envs_entails pre_envs_entails_eq. Qed.
-Arguments envs_entails {PROP} Δ Q%I : rename.
+Arguments envs_entails {PROP} Δ Q%I.
 Instance: Params (@envs_entails) 1 := {}.
 
 Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {