From 4cd7ccda12539447b0727487989fd08558c7ad95 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 14 Feb 2018 12:52:57 +0100
Subject: [PATCH] Add test for #146.

---
 theories/tests/proofmode_monpred.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index d44c52e1f..cf7d297f5 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -74,4 +74,24 @@ Section tests.
   Lemma test_absolutely_affine `{BiAffine PROP} P Q R :
     ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ R -∗ ∀ᵢ (P ∗ Q).
   Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
+
+  (* We do not use section variables to avoid coq bug #5735. *)
+  Instance BU : BUpd PROP. Admitted.
+  Instance FU : FUpd PROP. Admitted.
+  Instance FUF : FUpdFacts PROP. Admitted.
+
+  Lemma test_apply_fupd_intro_mask E1 E2 P :
+    E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
+  Proof.
+    iIntros.
+    (* FIXME : a (PROP:=...) is needed. See #146. *)
+    Fail iApply fupd_intro_mask.
+    by iApply (fupd_intro_mask (PROP:=monPredSI)).
+  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 *)
+  Qed.
 End tests.
-- 
GitLab