From 74dfa8b6dd441c5b7f23a0a41aaac44edbad6fb8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 19 Feb 2018 18:06:20 +0100
Subject: [PATCH] core comment

---
 theories/base_logic/lib/core.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index f77e95978..f64ad81cf 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.
-- 
GitLab