Commit d3556db2 authored by Ralf Jung's avatar Ralf Jung

fix awp_apply error message

parent 1f9c5efc
......@@ -17,10 +17,7 @@
The command has indeed failed with message:
Tactic failure: iAuIntro: not all spatial assumptions are laterable.
The command has indeed failed with message:
Tactic failure: wp_apply: cannot apply
(<<< ∀ (v : val) (q : Qp), ?Goal ↦{q} v >>>
! #?Goal @ ⊤
<<< ?Goal ↦{q} v, RET v >>>).
Tactic failure: iAuIntro: not all spatial assumptions are laterable.
"printing"
: string
1 subgoal
......
......@@ -30,7 +30,7 @@ Section error.
Restart.
iIntros "HP". Fail awp_apply load_spec.
Abort.
End error.
End error.
(* Test if AWP and the AU obtained from AWP print. *)
......
......@@ -435,9 +435,11 @@ the context, which is intended to be the non-laterable assertions that iAuIntro
would choke on. You get them all back in the continuation of the atomic
operation. *)
Tactic Notation "awp_apply" open_constr(lem) :=
wp_apply_core lem (fun H => iApplyHyp H; last iAuIntro).
(wp_apply_core lem (fun H => iApplyHyp H));
last iAuIntro.
Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
wp_apply_core lem (fun H => iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H; last iAuIntro]).
(wp_apply_core lem (fun H => iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H]));
last iAuIntro.
Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
let Htmp := iFresh in
......
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