From cc95f0fbcc93520655c12af59f7d174e12604406 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 7 Feb 2018 11:19:31 +0100
Subject: [PATCH] Test case for `iAlways` and the `absolutely` modality.

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

diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 628a1e1a1..d44c52e1f 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -67,4 +67,11 @@ Section tests.
   Proof.
     iIntros "H HP". by iApply "H".
   Qed.
+
+  Lemma test_absolutely P Q : âˆ€áµ¢ emp -âˆ— âˆ€áµ¢ P -âˆ— âˆ€áµ¢ Q -âˆ— âˆ€áµ¢ (P âˆ— Q).
+  Proof. iIntros "#? HP HQ". iAlways. by iSplitL "HP". Qed.
+
+  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.
 End tests.
-- 
GitLab