From fdeea0b83100ad8f6862b5561abdef6280c90453 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Apr 2023 16:02:17 +0200
Subject: [PATCH] Group `monpred` BI instances together.

---
 iris/bi/monpred.v | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index f5a8e0d07..5421efc91 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -553,6 +553,18 @@ Section instances.
     @monPred_defs.monPred_in_unseal).
   Ltac unseal := rewrite !monPred_unseal /=.
 
+  Global Instance monPred_bi_persistently_forall :
+    BiPersistentlyForall PROP → BiPersistentlyForall monPredI.
+  Proof. intros ? A φ. split=> /= i. unseal. by apply persistently_forall_2. Qed.
+
+  Global Instance monPred_bi_pure_forall :
+    BiPureForall PROP → BiPureForall monPredI.
+  Proof. intros ? A φ. split=> /= i. unseal. by apply pure_forall_2. Qed.
+
+  Global Instance monPred_bi_later_contractive :
+    BiLaterContractive PROP → BiLaterContractive monPredI.
+  Proof. intros ? n. unseal=> P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
+
   Global Instance monPred_bi_embed_emp : BiEmbedEmp PROP monPredI.
   Proof. split. by unseal. Qed.
 
@@ -719,16 +731,6 @@ Section bi_facts.
   Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
   Proof. solve_proper. Qed.
 
-  Global Instance monPred_persistently_forall :
-    BiPersistentlyForall PROP → BiPersistentlyForall monPredI.
-  Proof. intros ? A φ. split=> /= i. unseal. by apply persistently_forall_2. Qed.
-
-  Global Instance monPred_pure_forall : BiPureForall PROP → BiPureForall monPredI.
-  Proof. intros ? A φ. split=> /= i. unseal. by apply pure_forall_2. Qed.
-
-  Global Instance monPred_later_contractive :
-    BiLaterContractive PROP → BiLaterContractive monPredI.
-  Proof. intros ? n. unseal=> P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
   Global Instance monPred_bi_löb : BiLöb PROP → BiLöb monPredI.
   Proof. rewrite {2}/BiLöb; unseal=> ? P HP; split=> i /=. apply löb_weak, HP. Qed.
   Global Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI.
-- 
GitLab