Commit 39e504e3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tweak error message and test case of `iLöb`.

parent 6c1297e7
......@@ -621,10 +621,10 @@ k is used in hypothesis Hk.
: string
The command has indeed failed with message:
Tactic failure: iRevert: k is used in hypothesis "Hk".
"iLöb_no_bi"
"iLöb_no_BiLöb"
: string
The command has indeed failed with message:
Tactic failure: iLöb: Löb induction not supported for this BI.
Tactic failure: iLöb: no 'BiLöb' instance found.
"test_pure_name"
: string
1 subgoal
......
......@@ -1127,8 +1127,8 @@ Section error_tests_bi.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Check "iLöb_no_bi".
Lemma iLöb_no_bi P : P.
Check "iLöb_no_BiLöb".
Lemma iLöb_no_BiLöb P : P.
Proof. Fail iLöb as "IH". Abort.
End error_tests_bi.
......
......@@ -2534,7 +2534,7 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
refine should use the other unification algorithm, which should
not have this issue. *)
notypeclasses refine (tac_löb _ IH _ _ _ _);
[iSolveTC || fail "iLöb: Löb induction not supported for this BI"
[iSolveTC || fail "iLöb: no 'BiLöb' instance found"
|reflexivity || fail "iLöb: spatial context not empty, this should not happen"
|pm_reduce;
lazymatch goal with
......
Markdown is supported
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