diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 3334e0bcfff072af0a98a438129e2ae1765b9a99..32aea02680415511fa415d29df37b00eb65f4854 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -11,7 +11,7 @@ Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ
   wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P).
 Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
 Definition uPred_fupd := uPred_fupd_aux.(unseal).
-Arguments uPred_fupd {_ _}.
+Arguments uPred_fupd {Σ _}.
 Definition uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
 Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
 
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 2014cd67df3936a57c128d3e9861fd556757b6f0..aea6c15e00be918a9ba0e3ed9f7d54ba88caa5d8 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -75,8 +75,8 @@ Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
   gen_heap_name : gname;
   gen_meta_name : gname
 }.
-Arguments gen_heap_name {_ _ _ _ _} _ : assert.
-Arguments gen_meta_name {_ _ _ _ _} _ : assert.
+Arguments gen_heap_name {L V Σ _ _} _ : assert.
+Arguments gen_meta_name {L V Σ _ _} _ : assert.
 
 Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
   gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V));
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 817e5473ba519e5779154d0ccf7ca91a207d112e..bea7c66396f0ac47a3191c5da84fc066bc647771 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -89,7 +89,7 @@ End definition.
 (** Seal it *)
 Definition atomic_update_aux : seal (@atomic_update_def). Proof. by eexists. Qed.
 Definition atomic_update := atomic_update_aux.(unseal).
-Arguments atomic_update {_ _ _ _}.
+Arguments atomic_update {PROP _ TA TB}.
 Definition atomic_update_eq : @atomic_update = _ := atomic_update_aux.(seal_eq).
 
 Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 380ef4f3cc099a8ff92bcbe21897a969965f818f..dbba9257bf239dbd7e05acc6d8890402a15dafce 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -61,7 +61,7 @@ Definition twp_def `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness
   := λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
 Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
 Definition twp' := twp_aux.(unseal).
-Arguments twp' {_ _ _}.
+Arguments twp' {Λ Σ _}.
 Existing Instance twp'.
 Definition twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _.
 Proof. rewrite -twp_aux.(seal_eq) //. Qed.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 916f502f1755285dc2aa362a5fc41cc03445c76a..44f06bd7c9caccf4261103026914cccce20c3d0d 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -48,7 +48,7 @@ Definition wp_def `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness :=
   λ s : stuckness, fixpoint (wp_pre s).
 Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
 Definition wp' := wp_aux.(unseal).
-Arguments wp' {_ _ _}.
+Arguments wp' {Λ Σ _}.
 Existing Instance wp'.
 Definition wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
 Proof. rewrite -wp_aux.(seal_eq) //. Qed.