diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index d070516b97f2ffe3f4a9a10e880d250b21fffbc6..4cf762d772d2c4519e702088fe58858dbd0eeeb2 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -5,7 +5,14 @@ Import uPred.
 
 (** The "core" of an assertion is its maximal persistent part.
     It can be defined entirely within the logic... at least
-    in the shallow embedding. *)
+    in the shallow embedding.
+    WARNING: The function "coreP" is NOT NON-EXPANSIVE.
+    This is because the turnstile is not non-expansive as a function
+    from iProp to (discreteC Prop).
+    To obtain a core that's non-expansive, we would have to add another
+    modality to the logic: a box that removes access to *all* resources,
+    not just restricts access to the core.
+*)
 
 Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
   (∀ `(!PersistentP Q), ⌜P ⊢ Q⌝ → Q)%I.