Commit 225b639d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove useless eta expansion.

parent 845d6b1d
......@@ -90,7 +90,7 @@ Notation "'skipᶜ'" := (c_ret #()).
Definition c_seq_bind : val := λ: "x" "f",
"a" ←ᶜ "x" ;;
c_atomic_env (λ: "env", mset_clear "env") ;;
c_atomic_env mset_clear ;;
"f" "a".
Notation "x ←ᶜ e1 ;ᶜ e2" :=
(c_seq_bind e1%E (λ: x, e2)%E)%E
......@@ -393,7 +393,7 @@ Section proofs.
cwp_pures. iApply cwp_bind.
iApply cwp_atomic_env. iIntros (env) "Henv $". iApply wp_fupd.
iDestruct "Henv" as (X σ _) "[Hlocks Hσ]".
wp_lam. wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
wp_apply (mset_clear_spec with "Hlocks"); iIntros "Hlocks".
rewrite U_eq. iDestruct "H" as (us) "[Hus H]".
iInduction us as [|[ul [uq uv]] us] "IH" forall (σ); simpl.
- iModIntro. iSplitR "H".
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