Commit d2c226e7 authored by Ralf Jung's avatar Ralf Jung
Browse files

prepare for f_equiv change

parent 38392de4
......@@ -473,7 +473,7 @@ Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
Proof.
rewrite envs_entails_eq. intros. rewrite -twp_bind.
eapply wand_apply; first exact: twp_cmpxchg_fail.
rewrite envs_lookup_split //=. by do 2 f_equiv.
rewrite envs_lookup_split //=. simpl. by do 2 f_equiv.
Qed.
Lemma tac_wp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
......
Supports Markdown
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