From 4ee23161eabe872359a22cd84b4dd03c88ea66c6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 11 Nov 2017 21:39:17 +0100
Subject: [PATCH] Proof mode name fixes (in preparation of Iris !83).

---
 theories/lifetime/na_borrow.v         | 2 +-
 theories/typing/lib/refcell/refcell.v | 2 +-
 theories/typing/lib/rwlock/rwlock.v   | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index e3864ebd..bac68ad6 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -52,7 +52,7 @@ Section na_bor.
 
   Lemma na_bor_shorten κ κ': κ ⊑ κ' -∗ &na{κ',tid,N}P -∗ &na{κ,tid,N}P.
   Proof.
-    iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
+    iIntros "Hκκ' H". iDestruct "H" as (i) "[H ?]". iExists i. iFrame.
     iApply (idx_bor_shorten with "Hκκ' H").
   Qed.
 
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 5b7d94c9..efdb9d10 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -127,7 +127,7 @@ Section refcell.
     iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, refcell_inv tid l γ κ ty)%I with "[> -Hclose]"
       as "[$ HQ]"; last first.
     { iMod ("Hclose" with "[] HQ") as "[Hb $]".
-      - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
+      - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(H & _ & _)".
         iExists _. iIntros "{$H}!%". destruct st as [[?[|[]|]]|]; simpl; lia.
       - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
         iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 6b42693d..67d1092e 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -122,7 +122,7 @@ Section rwlock.
     iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, rwlock_inv tid l γ κ ty)%I with "[> -Hclose]"
       as "[$ HQ]"; last first.
     { iMod ("Hclose" with "[] HQ") as "[Hb $]".
-      - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
+      - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(H & _ & _)".
         iExists _. iIntros "{$H}!%". destruct st as [[|[[]?]|]|]; simpl; lia.
       - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
         iExists κ, γ. iSplitR. by iApply lft_incl_refl. iApply bor_share; try done.
-- 
GitLab