diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v index f257ff719c61eac5f285e58fc3742f39ebe02c6e..44a04c5b58a93a679dd3fafb1703e13aa1ad5ae7 100644 --- a/theories/tests/proofmode.v +++ b/theories/tests/proofmode.v @@ -142,7 +142,7 @@ Proof. iSpecialize ("H" $! _ [#10]). done. Qed. -Lemma test_eauto_iFramE P Q R `{!Persistent R} : +Lemma test_eauto_iFrame P Q R `{!Persistent R} : P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False. Proof. eauto 10 with iFrame. Qed.