diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index dbd4d37864990abd61508d649ddb61912d7d42f4..a2ddcee2a2dbc4fc6a4ab3428d689d94f3e0e65e 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -430,7 +430,8 @@ Tactic Notation "iApply" open_constr(lem) :=
     [iExact H
     |eapply tac_apply with _ H _ _ _;
       [env_cbv; reflexivity
-      |apply _
+      |let P := match goal with |- IntoWand ?P _ _ => P end in
+       apply _ || fail 1 "iApply: cannot apply" P
       |lazy beta (* reduce betas created by instantiation *)]]).
 
 (** * Revert *)