diff --git a/base_logic/lib/own.v b/base_logic/lib/own.v
index d6bde8ab9fe33f57f16c1ea7e3a8ba3e7e447558..103bdca73e0c875b98f9c410027d6386b04b4449 100644
--- a/base_logic/lib/own.v
+++ b/base_logic/lib/own.v
@@ -139,7 +139,7 @@ Arguments own_update {_ _} [_] _ _ _ _.
 Arguments own_update_2 {_ _} [_] _ _ _ _ _.
 Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
 
-Lemma own_empty `{inG Σ (A:ucmraT)} γ : True ==∗ own γ ∅.
+Lemma own_empty A `{inG Σ (A:ucmraT)} γ : True ==∗ own γ ∅.
 Proof.
   rewrite ownM_empty !own_eq /own_def.
   apply bupd_ownM_update, iprod_singleton_update_empty.
diff --git a/base_logic/lib/thread_local.v b/base_logic/lib/thread_local.v
index 7fa268625c07a94e83c3c791c4ed9157499f9839..57b65ac024bd952136c410547ae715a989776ea6 100644
--- a/base_logic/lib/thread_local.v
+++ b/base_logic/lib/thread_local.v
@@ -54,7 +54,7 @@ Section proofs.
   Lemma tl_inv_alloc tid E N P : ▷ P ={E}=∗ tl_inv tid N P.
   Proof.
     iIntros "HP".
-    iMod (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
+    iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
     iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
     { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
       apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ nclose N)).
diff --git a/base_logic/lib/wsat.v b/base_logic/lib/wsat.v
index 78615f2660da12dec6609192a9cc92acf46cea6e..30849c8328f8f11f01eec1ed7406f8a183adeac6 100644
--- a/base_logic/lib/wsat.v
+++ b/base_logic/lib/wsat.v
@@ -53,7 +53,7 @@ Global Instance ownI_persistent i P : PersistentP (ownI i P).
 Proof. rewrite /ownI. apply _. Qed.
 
 Lemma ownE_empty : True ==∗ ownE ∅.
-Proof. by rewrite (own_empty (A:=coPset_disjUR) enabled_name). Qed.
+Proof. by rewrite (own_empty (coPset_disjUR) enabled_name). Qed.
 Lemma ownE_op E1 E2 : E1 ⊥ E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2.
 Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
 Lemma ownE_disjoint E1 E2 : ownE E1 ∗ ownE E2 ⊢ E1 ⊥ E2.
@@ -68,7 +68,7 @@ Lemma ownE_singleton_twice i : ownE {[i]} ∗ ownE {[i]} ⊢ False.
 Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
 
 Lemma ownD_empty : True ==∗ ownD ∅.
-Proof. by rewrite (own_empty (A:=gset_disjUR _) disabled_name). Qed.
+Proof. by rewrite (own_empty (gset_disjUR positive) disabled_name). Qed.
 Lemma ownD_op E1 E2 : E1 ⊥ E2 → ownD (E1 ∪ E2) ⊣⊢ ownD E1 ∗ ownD E2.
 Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
 Lemma ownD_disjoint E1 E2 : ownD E1 ∗ ownD E2 ⊢ E1 ⊥ E2.
@@ -126,7 +126,7 @@ Lemma ownI_alloc φ P :
   wsat ∗ ▷ P ==∗ ∃ i, ■ (φ i) ∗ wsat ∗ ownI i P.
 Proof.
   iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
-  iMod (own_empty (A:=gset_disjUR positive) disabled_name) as "HE".
+  iMod (own_empty (gset_disjUR positive) disabled_name) as "HE".
   iMod (own_updateP with "HE") as "HE".
   { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
     intros E. destruct (Hfresh (E ∪ dom _ I))