From dfa9e843477b3a802c47771b4d40e466486037fc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Aug 2016 17:09:00 +0200
Subject: [PATCH] Better error message when iVs is used in non-view shift goal.
---
proofmode/tactics.v | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 49e373371..dcf66b391 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -508,14 +508,15 @@ Tactic Notation "iTimeless" constr(H) :=
Tactic Notation "iVsIntro" :=
eapply tac_vs_intro;
[let P := match goal with |- FromVs ?P _ => P end in
- apply _ || fail "iVsIntro:" P "not a viewshift"|].
+ apply _ || fail "iVsIntro:" P "not a view shift"|].
Tactic Notation "iVsCore" constr(H) :=
eapply tac_vs_elim with _ H _ _ _ _;
[env_cbv; reflexivity || fail "iVs:" H "not found"
|let P := match goal with |- ElimVs ?P _ _ _ => P end in
- let Q := match goal with |- ElimVs _ _ _ ?Q => Q end in
- apply _ || fail "iVs: cannot eliminate" H ":" P "in" Q
+ let Q := match goal with |- ElimVs _ _ ?Q _ => Q end in
+ apply _ || fail "iVs: cannot run" H ":" P "in" Q
+ "because the goal or hypothesis is not a view shift"
|env_cbv; reflexivity|].
(** * Basic destruct tactic *)
--
GitLab