Commit 2a909937 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Improve error message of iInv when mask condition cannot be solved.

parent f69cdc8c
...@@ -8,7 +8,8 @@ Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) := ...@@ -8,7 +8,8 @@ Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
let pat := constr:(IList [[IName Htmp; patback]]) in let pat := constr:(IList [[IName Htmp; patback]]) in
iVs (inv_open _ N with "[#]") as pat; iVs (inv_open _ N with "[#]") as pat;
[idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac]; [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) := Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestruct H as pat) Hclose. iInvCore N as (fun H => iDestruct H as pat) Hclose.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment