Commit 19af143a authored by Robbert Krebbers's avatar Robbert Krebbers

Better error message when iApply fails.

The error message accidentally got removed in e0789039.
parent 2cd0ddf0
......@@ -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 *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment