diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 68920fb9a8678799eed5a46c2ab4edb7ae9534b7..68ac02005f481b7dda6bf611da17874c48434bc1 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -21,7 +21,7 @@ Class FrameMonPredAt {I : biIndex} {PROP : bi} (p : bool) (i : I)
       (𝓡 : PROP) (P : monPred I PROP) (𝓠 : PROP) :=
   frame_monPred_at : □?p 𝓡 ∗ 𝓠 -∗ P i.
 Arguments FrameMonPredAt {_ _} _ _ _%I _%I _%I.
-Hint Mode FrameMonPredAt + + + + ! ! - : typeclass_instances.
+Hint Mode FrameMonPredAt + + + - ! ! - : typeclass_instances.
 
 Section modalities.
   Context {I : biIndex} {PROP : bi}.