Commit b300eb97 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'robbert/issue260' into 'master'

Fix issue #260: Error message when iLöb used on non-SBI

Closes #260

See merge request iris/iris!302
parents 77ed4519 bdb7b828
Pipeline #18981 passed with stage
in 19 minutes and 45 seconds
......@@ -706,3 +706,14 @@ The command has indeed failed with message:
In nested Ltac calls to "iRevert ( (ident) )" and
"iForallRevert (ident)", last call failed.
Tactic failure: iRevert: k is used in hypothesis "Hk".
"iLöb_no_sbi"
: string
The command has indeed failed with message:
In nested Ltac calls to "iLöb as (constr)",
"iLöbRevert (constr) with (tactic3)",
"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go",
"tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
"∗" with tac), "iRevertIntros (constr) with (tactic3)",
"iRevertIntros_go", "tac" (bound to iLöbCore as IH),
"tac" (bound to iLöbCore as IH) and "iLöbCore as (constr)", last call failed.
Tactic failure: iLöb: not a step-indexed BI entailment.
......@@ -928,3 +928,12 @@ Check "iRevert_dep_var".
Lemma iRevert_dep_var (k : nat) (Φ : nat PROP) : Φ k - Φ (S k).
Proof. iIntros "Hk". Fail iRevert (k). Abort.
End error_tests.
Section error_tests_bi.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Check "iLöb_no_sbi".
Lemma iLöb_no_sbi P : P.
Proof. Fail iLöb as "IH". Abort.
End error_tests_bi.
......@@ -2445,7 +2445,9 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
(* apply is sometimes confused wrt. canonical structures search.
refine should use the other unification algorithm, which should
not have this issue. *)
notypeclasses refine (tac_löb _ IH _ _ _);
first
[notypeclasses refine (tac_löb _ IH _ _ _)
|fail 1 "iLöb: not a step-indexed BI entailment"];
[reflexivity || fail "iLöb: spatial context not empty, this should not happen"
|pm_reduce;
lazymatch goal with
......@@ -2653,7 +2655,9 @@ Local Ltac iRewriteFindPred :=
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
iPoseProofCore lem as true (fun Heq =>
eapply (tac_rewrite _ Heq _ _ lr);
first
[eapply (tac_rewrite _ Heq _ _ lr)
|fail 1 "iRewrite: not a step-indexed BI entailment"];
[pm_reflexivity ||
let Heq := pretty_ident Heq in
fail "iRewrite:" Heq "not found"
......
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