From a98a72de1b620b069edac38bba343ba49fe4a7be Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 29 Sep 2023 11:53:21 +0200
Subject: [PATCH] frame_and comment

---
 iris/proofmode/class_instances_frame.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index e3c78d51e..c391c5bc5 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -106,6 +106,9 @@ Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R
   Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q | 2.
 Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
 
+(* For framing below [∧], we can frame [R] away in *both* conjuncts
+(unlike with [∗] where we can only frame it in one conjunct).
+We require at least one of those to make progress though. *)
 Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
   MaybeFrame p R P1 Q1 progress1 →
   MaybeFrame p R P2 Q2 progress2 →
-- 
GitLab