From 93644298298250c0df8f3314ab50fd4dc51e434c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 13 Apr 2016 00:39:04 +0200
Subject: [PATCH] Better error message in case iRevert fails.
---
proofmode/tactics.v | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 061323872..e227226f2 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -368,10 +368,11 @@ Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
Tactic Notation "iRevert" "★" := eapply tac_revert_spatial; env_cbv.
Tactic Notation "iForallRevert" ident(x) :=
- match type of x with
- | _ : Prop => revert x; apply tac_pure_revert
+ let A := type of x in
+ lazymatch type of A with
+ | Prop => revert x; apply tac_pure_revert
| _ => revert x; apply tac_forall_revert
- end.
+ end || fail "iRevert: cannot revert" x.
Tactic Notation "iImplRevert" constr(H) :=
eapply tac_revert with _ H _ _; (* (i:=H) *)
--
GitLab