From 2dfb8987f5ca0fb63b8ac9314692043f21ba204d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 12 Feb 2017 00:33:42 +0100
Subject: [PATCH] Better error message for iSpecialize.
---
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 715f44171..b1d0ffd97 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -275,7 +275,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
eapply tac_forall_specialize with _ H _ _ _ x; (* (i:=H) (a:=x) *)
[env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
|let P := match goal with |- IntoForall ?P _ => P end in
- apply _ || fail 1 "iSpecialize:" P "not a forall or not a forall of the right type"
+ apply _ || fail 1 "iSpecialize: cannot instantiate" P "with" x
|env_cbv; reflexivity|go xs]
end in
go xs.
--
GitLab