diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 87772c5fb5cbbbf34da5fc7276214428eaa36565..0ee9a0622f8229cbadb33f88e252f5fa3a145929 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1937,7 +1937,7 @@ Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(
    iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
 
 Tactic Notation "iAccu" :=
-  eapply tac_accu; env_reflexivity.
+  eapply tac_accu; [env_reflexivity || fail "iAccu: not an evar."].
 
 Hint Extern 0 (_ ⊢ _) => iStartProof.