From 98d8373b8b3167a201a3e3ff98fcdeb5b3c83bce Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 14 Feb 2018 14:02:17 +0100
Subject: [PATCH] Fix build.

---
 theories/tests/proofmode_monpred.v | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index b0c24e0af..997f212c6 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -88,13 +88,10 @@ Section tests.
 
   Lemma test_apply_fupd_intro_mask E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
-  Proof.
-    iIntros. iApply fupd_intro_mask.
-  Qed.
+  Proof. iIntros. by iApply fupd_intro_mask. Qed.
   Lemma test_apply_fupd_intro_mask_2 E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
   Proof.
-    iIntros. iFrame.
-    by iApply fupd_intro_mask'. (* But no annotation is needed here *)
+    iIntros. iFrame. by iApply fupd_intro_mask'.
   Qed.
 End tests.
-- 
GitLab