From 93ddf98137d5d64a61f468a31648ca2cd1897d37 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 11 Nov 2017 00:33:26 +0100
Subject: [PATCH] Play more with anonymous introduction patterns in tests.

---
 theories/tests/proofmode.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 748c19512..b1cd8665d 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -30,7 +30,7 @@ Proof.
   iRight.
   iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)".
   iPoseProof "Hc" as "foo".
-  iRevert (a b) "Ha Hb". iIntros (b a) "Hb {foo} Ha".
+  iRevert (a b) "Ha Hb". iIntros (b a) "? {foo} Ha".
   iAssert (uPred_ownM (a â‹… core a)) with "[Ha]" as "[Ha #Hac]".
   { by rewrite cmra_core_r. }
   iIntros "{$Hac $Ha}".
@@ -98,7 +98,7 @@ Lemma test_very_fast_iIntros P :
 Proof. by iIntros. Qed.
 
 Lemma test_iDestruct_spatial_and P Q1 Q2 : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1.
-Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.
+Proof. iIntros "[H [? _]]". by iFrame. Qed.
 
 Lemma test_iFrame_pure (x y z : M) :
   ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
@@ -116,7 +116,7 @@ Qed.
 
 Lemma test_iSpecialize_auto_frame P Q R :
   (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
-Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
+Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
 
 (* Check coercions *)
 Lemma test_iExist_coercion (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x.
-- 
GitLab