Commit f530c3ec authored by Ralf Jung's avatar Ralf Jung

explain the awp_apply tactics a bit

parent 97f7dfb3
...@@ -375,11 +375,16 @@ Tactic Notation "wp_apply_core" open_constr(lem) tactic(tac) := ...@@ -375,11 +375,16 @@ Tactic Notation "wp_apply_core" open_constr(lem) tactic(tac) :=
end). end).
Tactic Notation "wp_apply" open_constr(lem) := Tactic Notation "wp_apply" open_constr(lem) :=
wp_apply_core lem (fun H => iApplyHyp H; try iNext; try wp_expr_simpl). wp_apply_core lem (fun H => iApplyHyp H; try iNext; try wp_expr_simpl).
(* Tactic tailored for atomic triples *) (** Tactic tailored for atomic triples: the first, simple one just runs iAuIntro
on the goal, as atomic triples always have an atomic update as their premise.
The second one additionaly does some framing: it gets rid of `Hs` from 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) := Tactic Notation "awp_apply" open_constr(lem) :=
wp_apply_core lem (fun H => iApplyHyp H; iAuIntro). wp_apply_core lem (fun H => iApplyHyp H; last iAuIntro).
Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) := 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; 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) := Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
let Htmp := iFresh in 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