From b9d25e994ffa3ebe5b422acd5d14aa675b722354 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 8 Dec 2020 00:10:01 +0100
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 tests/proofmode.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 0059095e0..3d150c749 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -251,7 +251,7 @@ Lemma test_iDestruct_exists_automatic_def P :
   an_exists P -∗ ∃ k, ▷^k P.
 Proof. iDestruct 1 as (?) "H". by iExists an_exists_name. Qed.
 
-(* use an Iris intro pattern [% H] to indicate iExistDestruct rather than (?) *)
+(* use an Iris intro pattern [% H] rather than (?) to indicate iExistDestruct *)
 Lemma test_exists_intro_pattern_anonymous P (Φ: nat → PROP) :
   P ∗ (∃ y:nat, Φ y) -∗ ∃ x, P ∗ Φ x.
 Proof.
-- 
GitLab