From a155cf6265ac6dc256480325c8f34075b8e5bb80 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Sep 2016 17:24:24 +0200
Subject: [PATCH] Better error message for iTimeless.
This solves issue 33.
---
proofmode/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 19db5a773..5ad5d7e8f 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -522,7 +522,7 @@ Tactic Notation "iTimeless" constr(H) :=
apply _ || fail "iTimeless: cannot remove later when goal is" Q
|env_cbv; reflexivity || fail "iTimeless:" H "not found"
|let P := match goal with |- IntoExceptLast ?P _ => P end in
- apply _ || fail "iTimeless:" P "not timeless"
+ apply _ || fail "iTimeless: cannot turn" P "into â—‡"
|env_cbv; reflexivity|].
(** * View shifts *)
--
GitLab