From 4417e0935b7955fef0eb7960e56dd5a51270d923 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 May 2018 18:04:11 +0200
Subject: [PATCH] move comment closer to where it is exploited

---
 theories/algebra/cmra.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d5fa7ff44..d0f5cffdd 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.
-- 
GitLab