Commit 9e2af621 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use `_` intro pattern for `True`.

parent 42943c18
......@@ -328,7 +328,7 @@ Section lemmas.
(* FIXME: Is there any way to prevent maybe_wand from unfolding?
It gets unfolded by env_cbv in the proofmode, ideally we'd like that
to happen only if one argument is a constructor. *)
iIntros (?) "Hinner >Hacc". iDestruct "Hacc" as (x') "[Hα' Hclose]".
iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x') "[Hα' Hclose]".
iMod ("Hinner" with "Hα'") as (x) "[Hα Hclose']".
iMod (fupd_intro_mask') as "Hclose''"; last iModIntro; first done.
iExists x. iFrame. iSplitWith "Hclose'".
......
......@@ -316,7 +316,7 @@ Section proofmode_classes.
α β γ (WP e @ s; E {{ Φ }})
(λ x, WP e @ s; E {{ v, |={E}=> β x (γ x -? Φ v) }})%I.
Proof.
iIntros (?) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iApply wp_fupd.
iApply (wp_wand with "(Hinner Hα)").
iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
......
......@@ -174,7 +174,7 @@ Global Instance elim_acc_fupd `{!BiFUpd PROP} {X} E1 E2 E α β mγ Q :
(|={E1,E}=> Q)
(λ x, |={E2}=> β x (mγ x -? |={E1,E}=> Q))%I.
Proof.
iIntros (?) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
Qed.
......
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