From f234569bc3738b82583f8a7bf3e7a0ccaac79553 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 23 Jan 2017 21:15:04 +0100
Subject: [PATCH] Better error message for iSpecialize.
---
theories/proofmode/tactics.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index a5f79c5fe..3dd911720 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -333,6 +333,8 @@ introduction pattern, which will be coerced into [true] when it solely contains
`#` or `%` patterns at the top-level. *)
Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
let p := intro_pat_persistent p in
+ let t :=
+ match type of t with string => constr:(ITrm t hnil "") | _ => t end in
lazymatch t with
| ITrm ?H ?xs ?pat =>
lazymatch type of H with
@@ -349,6 +351,7 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
end
| _ => fail "iSpecialize:" H "should be a hypothesis, use iPoseProof instead"
end
+ | _ => fail "iSpecialize:" t "should be a proof mode term"
end.
Tactic Notation "iSpecialize" open_constr(t) :=
--
GitLab