diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index 420105441c7a6b0a74f87df4260e3a279299a893..aa4b02911f8d9133da966fda7e268b2aafb68e64 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -309,7 +309,7 @@ Section gmap.
 
   Lemma big_opM_singleton f i x : ([^o map] k↦y ∈ {[i:=x]}, f k y) ≡ f i x.
   Proof.
-    rewrite -insert_empty big_opM_insert/=; last auto using lookup_empty.
+    rewrite -insert_empty big_opM_insert/=; last eauto using lookup_empty.
     by rewrite big_opM_empty right_id.
   Qed.
 
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 5755ff3a2e700fa4f462450827cdb6c8041fbd1f..979462cac1609f9e534186d4d825ff18c76c238e 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -644,8 +644,9 @@ Section ucmra.
 
   Global Instance cmra_unit_cmra_total : CmraTotal A.
   Proof.
-    intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?);
-      eauto using ucmra_unit_least, (core_id (ε:A)).
+    intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?); [..|by eauto].
+    - apply ucmra_unit_least.
+    - apply (core_id _).
   Qed.
   Global Instance empty_cancelable : Cancelable (ε:A).
   Proof. intros ???. by rewrite !left_id. Qed.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index a775a716ce3b5a73020eba9330b7af50ce41be66..199a7c16dc71c37ee8f8b018a411fa17a722507f 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -72,7 +72,7 @@ Section updates.
   Proof.
     rewrite /local_update /=. setoid_rewrite <-cmra_discrete_valid_iff.
     setoid_rewrite <-(λ n, discrete_iff n x).
-    setoid_rewrite <-(λ n, discrete_iff n x'). naive_solver eauto using 0.
+    setoid_rewrite <-(λ n, discrete_iff n x'). naive_solver eauto using O.
   Qed.
 
   Lemma local_update_valid0 x y x' y' :
diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index 5681a13992ef986d4cd1f1e3ecbb265c5a084090..aaf7e2a71d27226dbd5efc96962582f86c431dca 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -156,7 +156,7 @@ Proof.
     + by rewrite -Hm.
     + intros i. by rewrite -(dist_None n) -Hm dist_None.
   - intros [m [E|]]; rewrite namespace_map_valid_eq namespace_map_validN_eq /=
-      ?cmra_valid_validN; naive_solver eauto using 0.
+      ?cmra_valid_validN; naive_solver eauto using O.
   - intros n [m [E|]]; rewrite namespace_map_validN_eq /=;
       naive_solver eauto using cmra_validN_S.
   - split; simpl; [by rewrite assoc|by rewrite assoc_L].
@@ -188,7 +188,7 @@ Global Instance namespace_map_cmra_discrete :
 Proof.
   split; first apply _.
   intros [m [E|]]; rewrite namespace_map_validN_eq namespace_map_valid_eq //=.
-  naive_solver eauto using (cmra_discrete_valid m).
+  by intros [?%cmra_discrete_valid ?].
 Qed.
 
 Instance namespace_map_empty : Unit (namespace_map A) := NamespaceMap ε ε.
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index fe53c2a9cc010bb0ee245a4ea7866c9e231ac0a7..00462f7cbe04dbb4e4bcee91bc4deee530acaf92 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -114,13 +114,13 @@ Section total_updates.
     x ~~>: P ↔ ∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z).
   Proof.
     rewrite cmra_total_updateP; setoid_rewrite <-cmra_discrete_valid_iff.
-    naive_solver eauto using 0.
+    naive_solver eauto using O.
   Qed.
   Lemma cmra_discrete_update (x y : A) :
     x ~~> y ↔ ∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z).
   Proof.
     rewrite cmra_total_update; setoid_rewrite <-cmra_discrete_valid_iff.
-    naive_solver eauto using 0.
+    naive_solver eauto using O.
   Qed.
 End total_updates.
 End updates.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index e602f4a933a562490cd3a249e99cf501133923bb..b84f1a1ddc7f150cd5089d74c8216009b5d882b0 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -241,7 +241,7 @@ Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := uPred_exist_aux.(s
 
 Program Definition uPred_internal_eq_def {M} {A : ofeT} (a1 a2 : A) : uPred M :=
   {| uPred_holds n x := a1 ≡{n}≡ a2 |}.
-Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
+Solve Obligations with naive_solver eauto 2 using dist_le.
 Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). Proof. by eexists. Qed.
 Definition uPred_internal_eq {M A} := uPred_internal_eq_aux.(unseal) M A.
 Definition uPred_internal_eq_eq:
@@ -284,9 +284,7 @@ Definition uPred_plainly_eq :
 
 Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
-Next Obligation.
-  intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
-Qed.
+Solve Obligations with naive_solver eauto using uPred_mono, cmra_core_monoN.
 Definition uPred_persistently_aux : seal (@uPred_persistently_def). Proof. by eexists. Qed.
 Definition uPred_persistently {M} := uPred_persistently_aux.(unseal) M.
 Definition uPred_persistently_eq :
@@ -472,13 +470,13 @@ Qed.
 Lemma plainly_ne : NonExpansive (@uPred_plainly M).
 Proof.
   intros n P1 P2 HP.
-  unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
+  unseal; split=> n' x; split; apply HP; eauto using ucmra_unit_validN.
 Qed.
 
 Lemma persistently_ne : NonExpansive (@uPred_persistently M).
 Proof.
   intros n P1 P2 HP.
-  unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
+  unseal; split=> n' x; split; apply HP; eauto using cmra_core_validN.
 Qed.
 
 Lemma ownM_ne : NonExpansive (@uPred_ownM M).
@@ -587,7 +585,7 @@ Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
 Lemma persistently_elim P : □ P ⊢ P.
 Proof.
   unseal; split=> n x ? /=.
-  eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
+  eauto using uPred_mono, cmra_included_core, cmra_included_includedN.
 Qed.
 Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
 Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
@@ -607,7 +605,7 @@ Qed.
 Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
 Proof. intros HP; unseal; split=> n x ? /=. apply HP, ucmra_unit_validN. Qed.
 Lemma plainly_elim_persistently P : ■ P ⊢ □ P.
-Proof. unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. Qed.
+Proof. unseal; split; simpl; eauto using uPred_mono, ucmra_unit_leastN. Qed.
 Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P.
 Proof. unseal; split=> n x ?? //. Qed.
 
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index a118ac19e392b758c9326ba07429597fa39a4a32..a83570cd0f64da084a21fa96993188f151bdec91 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -151,7 +151,7 @@ Section sep_list.
   Lemma big_sepL_elem_of (Φ : A → PROP) l x `{!Absorbing (Φ x)} :
     x ∈ l → ([∗ list] y ∈ l, Φ y) ⊢ Φ x.
   Proof.
-    intros [i ?]%elem_of_list_lookup; eauto using (big_sepL_lookup (λ _, Φ)).
+    intros [i ?]%elem_of_list_lookup. by eapply (big_sepL_lookup (λ _, Φ)).
   Qed.
 
   Lemma big_sepL_fmap {B} (f : A → B) (Φ : nat → B → PROP) l :
@@ -657,7 +657,7 @@ Section and_list.
   Lemma big_andL_elem_of (Φ : A → PROP) l x :
     x ∈ l → ([∧ list] y ∈ l, Φ y) ⊢ Φ x.
   Proof.
-    intros [i ?]%elem_of_list_lookup; eauto using (big_andL_lookup (λ _, Φ)).
+    intros [i ?]%elem_of_list_lookup. by eapply (big_andL_lookup (λ _, Φ)).
   Qed.
 
   Lemma big_andL_fmap {B} (f : A → B) (Φ : nat → B → PROP) l :
@@ -756,7 +756,7 @@ Section or_list.
   Lemma big_orL_elem_of (Φ : A → PROP) l x :
     x ∈ l → Φ x ⊢ ([∨ list] y ∈ l, Φ y).
   Proof.
-    intros [i ?]%elem_of_list_lookup; eauto using (big_orL_lookup (λ _, Φ)).
+    intros [i ?]%elem_of_list_lookup; by eapply (big_orL_lookup (λ _, Φ)).
   Qed.
 
   Lemma big_orL_fmap {B} (f : A → B) (Φ : nat → B → PROP) l :
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index a0e9c245d4ecef085a320b99d8336e6cbf354b89..2fa0f289e93326d297fe160bdcf9ee912ed3ad36 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -182,7 +182,7 @@ Section language.
   Proof.
     rewrite /not_stuck -!not_eq_None_Some. intros [?|?].
     - auto using fill_not_val.
-    - destruct (decide (to_val e = None)); auto using reducible_fill_inv.
+    - destruct (decide (to_val e = None)); eauto using reducible_fill_inv.
   Qed.
 
   Lemma stuck_fill `{!@LanguageCtx Λ K} e σ :
diff --git a/theories/si_logic/siprop.v b/theories/si_logic/siprop.v
index 2256dc007e4fc4a5acb21a4d1e789f8254f08a3c..d1538b871aa6d7cebd53c48d23ca56b420bab475 100644
--- a/theories/si_logic/siprop.v
+++ b/theories/si_logic/siprop.v
@@ -100,7 +100,7 @@ Definition siProp_exist_eq: @siProp_exist = @siProp_exist_def := seal_eq siProp_
 
 Program Definition siProp_internal_eq_def {A : ofeT} (a1 a2 : A) : siProp :=
   {| siProp_holds n := a1 ≡{n}≡ a2 |}.
-Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
+Solve Obligations with naive_solver eauto 2 using dist_le.
 Definition siProp_internal_eq_aux : seal (@siProp_internal_eq_def). Proof. by eexists. Qed.
 Definition siProp_internal_eq {A} := unseal siProp_internal_eq_aux A.
 Definition siProp_internal_eq_eq: