From 854dcaaf140ab81029247106b833d2c35a39f124 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 1 May 2022 17:20:45 +0000
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 d67a8b9d1..fc2de8e85 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1115,7 +1115,7 @@ Lemma test_iApply_prettification3 (Ψ Φ : nat → PROP) :
   Ψ 11 -∗ Φ 10.
 Proof.
   iIntros (HP) "H".
-  iApply HP.
+  iApply HP. (* should be [Ψ (1 + 10)], without a beta redex *)
   Show.
   iApply "H".
 Qed.
-- 
GitLab