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

Fix error message of iApply.

parent 8927c9db
......@@ -565,7 +565,9 @@ Tactic Notation "iApply" open_constr(lem) :=
iPoseProofCore lem as false true (fun H => first
[iExact H
|go H
|lazymatch iTypeOf H with Some (_,?Q) => fail "iApply: cannot apply" Q end]).
|lazymatch iTypeOf H with
| Some (_,?Q) => fail 1 "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