From 6f712e1a0171bc13dca75b5e7816c96beece04ba Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 11 Sep 2020 17:42:30 +0200
Subject: [PATCH] improve [core] docs
---
theories/algebra/cmra.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index e8fd47444..668c23f5a 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -175,7 +175,8 @@ Class CmraTotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
Hint Mode CmraTotal ! : typeclass_instances.
(** The function [core] returns a dummy when used on CMRAs without total
-core. *)
+core. We only ever use this for [CmraTotal] CMRAs, but it is more convenient
+to not require that proof to be able to call this function. *)
Definition core `{PCore A} (x : A) : A := default x (pcore x).
Instance: Params (@core) 2 := {}.
--
GitLab