From 6edb48baa3ed11a9873b26d3b664031d5ac0f02e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 6 Jun 2021 12:42:32 +0200
Subject: [PATCH] add test for make_laterable iModIntro

---
 tests/proofmode.ref | 12 ++++++++++++
 tests/proofmode.v   |  8 ++++++++
 2 files changed, 20 insertions(+)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 745fd6013..ac5e9cf57 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -383,6 +383,18 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   default emp mP
   
+1 goal
+  
+  PROP : bi
+  H : BiAffine PROP
+  P, Q : PROP
+  H0 : Laterable Q
+  ============================
+  "HP" : â–· P
+  "HQ" : Q
+  --------------------------------------∗
+  ▷ P ∗ Q
+  
 "elim_mod_accessor"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 454da8ec7..afcfd89f2 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,3 +1,4 @@
+From iris.bi Require Import laterable.
 From iris.proofmode Require Import tactics intro_patterns.
 Set Default Proof Using "Type".
 
@@ -1079,6 +1080,13 @@ Proof.
   iIntros "[P _]". done.
 Qed.
 
+Lemma test_iModIntro_make_laterable `{BiAffine PROP} (P Q : PROP) :
+  Laterable Q →
+  P -∗ Q -∗ make_laterable (▷ P ∗ Q).
+Proof.
+  iIntros (?) "HP HQ". iModIntro. Show. by iFrame.
+Qed.
+
 End tests.
 
 Section parsing_tests.
-- 
GitLab