From 19af143a19998c625c0a3bd45388d7974bae4ff1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 20 Jan 2017 19:32:53 +0100
Subject: [PATCH] Better error message when iApply fails.
The error message accidentally got removed in e0789039.
---
theories/proofmode/tactics.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index dbd4d3786..a2ddcee2a 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -430,7 +430,8 @@ Tactic Notation "iApply" open_constr(lem) :=
[iExact H
|eapply tac_apply with _ H _ _ _;
[env_cbv; reflexivity
- |apply _
+ |let P := match goal with |- IntoWand ?P _ _ => P end in
+ apply _ || fail 1 "iApply: cannot apply" P
|lazy beta (* reduce betas created by instantiation *)]]).
(** * Revert *)
--
GitLab