Skip to content

GitLab

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

Fix error handling of iApply.

parent 3f1a2384
Hide whitespace changes
Inline Side-by-side
proofmode/tactics.v
View file @ f92cd3f3
......@@ -302,8 +302,8 @@ Tactic Notation "iApply" open_constr (lem) :=
iPoseProof lem as (fun H => repeat (iForallSpecialize H _); first
[iExact H
|eapply tac_apply with _ H _ _ _;
[env_cbv; reflexivity || fail "iApply:" lem "not found"
|apply _ || fail "iApply: cannot apply" lem|]]).
[env_cbv; reflexivity || fail 1 "iApply:" lem "not found"
|apply _ || fail 1 "iApply: cannot apply" lem|]]).
Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) "}" :=
iSpecialize H { x1 }; last iApply H.
Tactic Notation "iApply" open_constr (H) "{" open_constr(x1)
......@@ -335,8 +335,8 @@ Tactic Notation "iApply" open_constr (lem) constr(Hs) :=
iPoseProof lem Hs as (fun H => first
[iExact H
|eapply tac_apply with _ H _ _ _;
[env_cbv; reflexivity || fail "iApply:" lem "not found"
|apply _ || fail "iApply: cannot apply" lem|]]).
[env_cbv; reflexivity || fail 1 "iApply:" lem "not found"
|apply _ || fail 1 "iApply: cannot apply" lem|]]).
Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) "}" constr(Hs) :=
iSpecialize H { x1 }; last iApply H Hs.
Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2) "}"
......
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