Commit 3dc4997c authored by Ralf Jung's avatar Ralf Jung
Browse files

fix wp and wp> to be consistent with the other wp tactics (">" does *not* strip laters)

parent 1bf7e8f9
......@@ -33,10 +33,10 @@ Section LiftingTests.
nclose N E heap_ctx N || heap_e @ E {{ λ v, v = '2 }}.
Proof.
rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
wp> eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
wp_rec. wp> eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
wp_bin_op. wp> eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
wp_rec. wp> eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
wp eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
wp_rec. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
wp_bin_op. wp eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
wp_rec. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
by apply const_intro.
Qed.
......@@ -76,7 +76,7 @@ Section LiftingTests.
Lemma Pred_user E :
(True : iProp) || let: "x" := Pred '42 in Pred "x" @ E {{ λ v, v = '40 }}.
Proof.
intros. ewp> apply Pred_spec. wp_rec. ewp> apply Pred_spec. auto with I.
intros. ewp apply Pred_spec. wp_rec. ewp apply Pred_spec. auto with I.
Qed.
End LiftingTests.
......
......@@ -82,11 +82,11 @@ Tactic Notation "wp_focus" open_constr(efoc) :=
match e' with efoc => unify e' efoc; wp_bind K end)
end.
Tactic Notation "wp" tactic(tac) :=
Tactic Notation "wp" ">" tactic(tac) :=
match goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => wp_bind K; tac)
end.
Tactic Notation "wp" ">" tactic(tac) := (wp tac); wp_strip_later.
Tactic Notation "wp" tactic(tac) := (wp> tac); wp_strip_later.
(* In case the precondition does not match *)
Tactic Notation "ewp" tactic(tac) := wp (etransitivity; [|tac]).
......
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