From 2a909937c16302d1b986ed27b800fe0f775dfcf2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 30 Aug 2016 00:19:20 +0200
Subject: [PATCH] Improve error message of iInv when mask condition cannot be
solved.
---
proofmode/invariants.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
index 936545e29..d5813093e 100644
--- a/proofmode/invariants.v
+++ b/proofmode/invariants.v
@@ -8,7 +8,8 @@ Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
let pat := constr:(IList [[IName Htmp; patback]]) in
iVs (inv_open _ N with "[#]") as pat;
[idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
- [solve_ndisj|tac Htmp].
+ [solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
+ |tac Htmp].
Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestruct H as pat) Hclose.
--
GitLab