From 379aa18eb51e3fdb2018131e115a7406213b5279 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 25 Jan 2018 22:19:58 +0100
Subject: [PATCH] Add test.
---
theories/tests/proofmode_monpred.v | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 8532b4817..4281ec6ef 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -64,4 +64,9 @@ Section tests.
Proof.
iStartProof. iIntros (n) "$".
Qed.
+
+ Lemma test_embed_wand (P Q : PROP) : (⎡P⎤ -∗ ⎡Q⎤) -∗ ⎡P -∗ Q⎤ : monPred.
+ Proof.
+ iIntros "H HP". by iApply "H".
+ Qed.
End tests.
--
GitLab