diff --git a/algebra/cofe.v b/algebra/cofe.v
index 3d43b09e74edd725186d30275af741ed72d3bb97..0d35a88a0c3a5fc67aee6593afe105612c432a05 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -208,6 +208,8 @@ Section fixpoint.
 End fixpoint.
 
 (** Function space *)
+(* We make [cofe_fun] a definition so that we can register it as a canonical
+structure. *)
 Definition cofe_fun (A : Type) (B : cofeT) := A → B.
 
 Section cofe_fun.