From b81b27d3e38209aab3600e761919b36dc5af5116 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 22 Feb 2017 18:34:53 +0100
Subject: [PATCH] Fix error message of iApply.
---
theories/proofmode/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index a70bacbf2..cd4b76020 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -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) :=
--
GitLab