diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index f77e959783c87fe474bb6f9ee3f0cd58491852b1..f64ad81cfac2220e4dc1ed4635e40243f4f1e2af 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -3,7 +3,9 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
-(** The "core" of an assertion is its maximal persistent part. *)
+(** The "core" of an assertion is its maximal persistent part,
+ i.e. the conjunction of all persistent assertions that are weaker
+ than P (as in, implied by P). *)
Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
(∀ Q, ■ (P → □ Q) → □ Q)%I.
Instance: Params (@coreP) 1.