From ded3b67486832ed2f2aae24c8278f5203a609846 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Sep 2020 18:40:22 +0200
Subject: [PATCH] Comment.

---
 theories/proofmode/frame_instances.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index e158504c8..ff71e3a10 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -6,6 +6,15 @@ Import bi.
 
 (** This file defines the instances that make up the framing machinery. *)
 
+(** When framing below logical connectives/modalities, framing will perform
+some "clean up" to remove connectives/modalities if the result of framing is
+[True] or [emp]. For example, framing [P] in [P ∗ Q] or [<affine> P] will
+result in [Q] and [emp], respectively, instead of [emp ∗ Q] and [<affine> emp],
+respectively. One could imagine a smarter way of cleaning up, as implemented in
+https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/450 for some modalities,
+but that makes framing less predictable and might have some performance impact.
+Hence, we only perform such cleanup for [True] and [emp]. *)
+
 Section bi.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
-- 
GitLab