diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index b15ba0355e35f7999af0f38c93ff77809c049989..679db07daf2433af296e6fd92e04d7485510425a 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -33,6 +33,7 @@ Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P.
 Arguments timelessP {_} _ {_}.
 
 Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
+Hint Mode PersistentP - ! : typeclass_instances.
 Arguments persistentP {_} _ {_}.
 
 Module uPred.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 70130e8260ea2f7ecaebad4ceb0be5054bbfee12..8bc9ca71aa115c2084790b5d94d28a5b920089a3 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -104,7 +104,7 @@ Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
 Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
 Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
 Lemma own_valid_r γ a : own γ a ⊢ own γ a ∗ ✓ a.
-Proof. apply (uPred.always_entails_r _ _). apply own_valid. Qed.
+Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a.
 Proof. by rewrite comm -own_valid_r. Qed.