diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index dfbb381f88a6619bbac1cb4bb54e40067f978fc6..e8dfd8dc30271e85fd2acf7730e127f060e90b4f 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -623,7 +623,7 @@ Tactic Notation "iIntoValid" open_constr(t) :=
       let e' := eval unfold e in e in clear e; go (t e')
     | _ =>
       let tT' := eval cbv zeta in tT in apply (as_valid_1 tT');
-        [apply _ || fail "iPoseProof: not a uPred"|exact t]
+        [apply _ || fail "iPoseProof: not a BI assertion"|exact t]
     end in
   go t.