From 1f36e73436ae97baed09ae6edf28d012c95c1a4e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Nov 2016 16:59:59 +0100
Subject: [PATCH] Better error message when the argument of iSpecialize is not
a hypothesis.
---
proofmode/tactics.v | 22 +++++++++++++---------
1 file changed, 13 insertions(+), 9 deletions(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index c73e4d9bc..211dee6d4 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -338,15 +338,19 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) tactic(tac) :=
end in
lazymatch t with
| ITrm ?H ?xs ?pat =>
- lazymatch p with
- | true =>
- eapply tac_specialize_persistent_helper with _ H _ _ _;
- [env_cbv; reflexivity || fail "iSpecialize:" H "not found"
- |iSpecializeArgs H xs; iSpecializePat H pat; last (iExact H)
- |let Q := match goal with |- PersistentP ?Q => Q end in
- apply _ || fail "iSpecialize:" Q "not persistent"
- |env_cbv; reflexivity|tac H]
- | false => iSpecializeArgs H xs; iSpecializePat H pat; last (tac H)
+ lazymatch type of H with
+ | string =>
+ lazymatch p with
+ | true =>
+ eapply tac_specialize_persistent_helper with _ H _ _ _;
+ [env_cbv; reflexivity || fail "iSpecialize:" H "not found"
+ |iSpecializeArgs H xs; iSpecializePat H pat; last (iExact H)
+ |let Q := match goal with |- PersistentP ?Q => Q end in
+ apply _ || fail "iSpecialize:" Q "not persistent"
+ |env_cbv; reflexivity|tac H]
+ | false => iSpecializeArgs H xs; iSpecializePat H pat; last (tac H)
+ end
+ | _ => fail "iSpecialize:" H "should be a hypothesis, use iPoseProof instead"
end
end.
--
GitLab