add test for make_laterable iModIntro

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

tests/proofmode.v

+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.