From 25f1b8895c212ec2481bd493faa9cab7fce16b5c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Aug 2016 23:38:08 +0200
Subject: [PATCH] Document why cofe_fun is a definition.

---
 algebra/cofe.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index 3d43b09e7..0d35a88a0 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.
-- 
GitLab