diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d5fa7ff44bae720c437b58842998a56b85442b48..d0f5cffddae4dd32f4af0c050abf69f2a0c7d69f 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -170,11 +170,11 @@ Hint Mode IdFree + ! : typeclass_instances.
 Instance: Params (@IdFree) 1.
 
 (** * CMRAs whose core is total *)
-(** The function [core] may return a dummy when used on CMRAs without total
-core. *)
 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. *)
 Class Core (A : Type) := core : A → A.
 Hint Mode Core ! : typeclass_instances.
 Instance: Params (@core) 2.