From 0581fe45982f8e4a2df2b120858e6ba42b398a97 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 2 Feb 2018 11:47:11 +0100 Subject: [PATCH] Fix typo. --- theories/tests/proofmode.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v index f257ff719..44a04c5b5 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. -- GitLab