Commit be8849c2 authored by Robbert Krebbers's avatar Robbert Krebbers

Get rid of wp_value.

The tactic was doing something weird and only once used.
parent 290a45af
......@@ -27,8 +27,8 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
( v1 v2, Ψ1 v1 Ψ2 v2 - Φ (v1,v2)%V) -
WP par e {{ Φ }}.
Proof.
iIntros (?) "Hf1 Hf2 HΦ".
rewrite /par. wp_value. wp_let. wp_proj.
iIntros (<-%of_to_val) "Hf1 Hf2 HΦ".
rewrite /par /=. wp_let. wp_proj.
wp_apply (spawn_spec parN with "Hf1"); try wp_done; try solve_ndisj.
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
......
......@@ -24,14 +24,6 @@ Ltac wp_done :=
Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; simpl.
Tactic Notation "wp_value" :=
iStartProof;
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
| _ => fail "wp_value: not a wp"
end.
Lemma of_val_unlock v e : of_val v = e of_val (locked v) = e.
Proof. by unlock. Qed.
......
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