From fbc6b6b64c5b1c8ae923c09ddb1090cfca7b191f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 13 Apr 2017 12:59:52 +0200
Subject: [PATCH] Fix error message of iApply.
---
theories/proofmode/tactics.v | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 89c42bdc7..250475d29 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -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
+ end]).
(** * Revert *)
Local Tactic Notation "iForallRevert" ident(x) :=
--
GitLab