Commit b81b27d3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix error message of iApply.

parent 8bfa7c46
......@@ -441,7 +441,7 @@ Tactic Notation "iApply" open_constr(lem) :=
|lazy beta (* reduce betas created by instantiation *)]
|iSpecializePat H "[]"; last go H] in
iPoseProofCore lem as false true (fun H =>
first [iExact H|go H|iTypeOf H (fun Q => fail 1 "iApply: cannot apply" Q)]).
first [iExact H|go H|iTypeOf H (fun _ Q => fail "iApply: cannot apply" Q)]).
(** * Revert *)
Local Tactic Notation "iForallRevert" ident(x) :=
Supports Markdown
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