diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 19db5a773733508f916ce8098ca1ea8535ae35dd..5ad5d7e8f5579e1ce51e73d77dce312b4f1b70c2 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -522,7 +522,7 @@ Tactic Notation "iTimeless" constr(H) :=
      apply _ || fail "iTimeless: cannot remove later when goal is" Q
     |env_cbv; reflexivity || fail "iTimeless:" H "not found"
     |let P := match goal with |- IntoExceptLast ?P _ => P end in
-     apply _ || fail "iTimeless:" P "not timeless"
+     apply _ || fail "iTimeless: cannot turn" P "into â—‡"
     |env_cbv; reflexivity|].
 
 (** * View shifts *)