Commit 890b60e5 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix issue #260.

parent d6672184
...@@ -2445,7 +2445,9 @@ Tactic Notation "iLöbCore" "as" constr (IH) := ...@@ -2445,7 +2445,9 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
(* apply is sometimes confused wrt. canonical structures search. (* apply is sometimes confused wrt. canonical structures search.
refine should use the other unification algorithm, which should refine should use the other unification algorithm, which should
not have this issue. *) 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" [reflexivity || fail "iLöb: spatial context not empty, this should not happen"
|pm_reduce; |pm_reduce;
lazymatch goal with lazymatch goal with
...@@ -2653,7 +2655,9 @@ Local Ltac iRewriteFindPred := ...@@ -2653,7 +2655,9 @@ Local Ltac iRewriteFindPred :=
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) := Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
iPoseProofCore lem as true (fun Heq => 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 || [pm_reflexivity ||
let Heq := pretty_ident Heq in let Heq := pretty_ident Heq in
fail "iRewrite:" Heq "not found" 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