diff --git a/tests/proofmode.v b/tests/proofmode.v index 0059095e0df1cf30bbdfee1b677feacd57616ce9..3d150c749c3abd7c25871832d953722c8b1dcc55 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.