From ad005c0cd479efcb9ed38595013308c070521938 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Feb 2018 01:16:40 +0100
Subject: [PATCH] Proper error message when `//` spec pattern fails.
---
theories/proofmode/tactics.v | 14 +++++++++++---
1 file changed, 11 insertions(+), 3 deletions(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 2ae625a29..4a1a64e0c 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -475,6 +475,14 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
apply _ ||
let P := match goal with |- IntoWand _ _ ?P _ _ => P end in
fail "iSpecialize:" P "not an implication/wand" in
+ let solve_done d :=
+ lazymatch d with
+ | true =>
+ done ||
+ let Q := match goal with |- envs_entails _ ?Q => Q end in
+ fail "iSpecialize: cannot solve" Q "using done"
+ | false => idtac
+ end in
let rec go H1 pats :=
lazymatch pats with
| [] => idtac
@@ -498,7 +506,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
let Q := match goal with |- FromPure _ ?Q _ => Q end in
fail "iSpecialize:" Q "not pure"
|env_reflexivity
- |done_if d (*goal*)
+ |solve_done d (*goal*)
|go H1 pats]
| SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _ _;
@@ -509,7 +517,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
fail "iSpecialize:" Q "not persistent"
|apply _
|env_reflexivity
- |iFrame Hs_frame; done_if d (*goal*)
+ |iFrame Hs_frame; solve_done d (*goal*)
|go H1 pats]
| SGoal (SpecGoal GPersistent _ _ _ _) :: ?pats =>
fail "iSpecialize: cannot select hypotheses for persistent premise"
@@ -525,7 +533,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
|env_reflexivity ||
let Hs' := iMissingHyps Hs' in
fail "iSpecialize: hypotheses" Hs' "not found"
- |iFrame Hs_frame; done_if d (*goal*)
+ |iFrame Hs_frame; solve_done d (*goal*)
|go H1 pats]
| SAutoFrame GPersistent :: ?pats =>
eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
--
GitLab