From f92cd3f325ca47746dcc6a6009dbe112e59ef268 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Apr 2016 15:32:33 +0200
Subject: [PATCH] Fix error handling of iApply.
---
proofmode/tactics.v | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index e227226f2..6a0051416 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -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) "}"
--
GitLab