diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 97df3d6323e9e719bff7130b4d3ee5892a829aad..eca1b60943b0ab91b4b7762c649f8266cb3c43c5 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -6,7 +6,10 @@ Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
       (P : monPred I PROP) (𝓟 : PROP) :=
   make_monPred_at : P i ⊣⊢ 𝓟.
 Arguments MakeMonPredAt {_ _} _ _%I _%I.
-Hint Mode MakeMonPredAt + + - ! - : typeclass_instances.
+(** Since [MakeMonPredAt] is used by [AsEmpValid] to import lemmas into the
+proof mode, the index [I] and BI [PROP] often contain evars. Hence, it is
+important to use the mode [!] also for the first two arguments. *)
+Hint Mode MakeMonPredAt ! ! - ! - : typeclass_instances.
 
 Class IsBiIndexRel {I : biIndex} (i j : I) := is_bi_index_rel : i ⊑ j.
 Hint Mode IsBiIndexRel + - - : typeclass_instances.