From 9e2af621d8a8a4ccfa4240162be802620543573b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Jan 2021 09:49:43 +0100
Subject: [PATCH] Use `_` intro pattern for `True`.

---
 iris/bi/lib/atomic.v                     | 2 +-
 iris/program_logic/weakestpre.v          | 2 +-
 iris/proofmode/class_instances_updates.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 9c360274f..a7272ddc2 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -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'".
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index a030d348e..1123c57fa 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -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".
diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 63b0566a3..5fd7fea8b 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -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.
-- 
GitLab