From 8b4630b405c851b1f7097f2cd0954bc6dc10c45c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 5 Dec 2017 20:10:56 +0100
Subject: [PATCH] typeclass comments

---
 theories/base.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 532e7467..c30bbe82 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -119,8 +119,9 @@ Instance: @PreOrder A (=).
 Proof. split; repeat intro; congruence. Qed.
 
 (** ** Setoid equality *)
-(** We define an operational type class for setoid equality. This is based on
-(Spitters/van der Weegen, 2011). *)
+(** We define an operational type class for setoid equality, i.e., the
+"canonical" equivalence for a type. The typeclass is tied to the \equiv
+symbol. This is based on (Spitters/van der Weegen, 2011). *)
 Class Equiv A := equiv: relation A.
 (* No Hint Mode set because of Coq bug #5735
 Hint Mode Equiv ! : typeclass_instances. *)
@@ -1118,6 +1119,8 @@ Notation "½" := half : stdpp_scope.
 Notation "½*" := (fmap (M:=list) half) : stdpp_scope.
 
 (** * Notations for lattices. *)
+(** SqSubsetEq registers the "canonical" partial order for a type, and is used
+for the \sqsubseteq symbol. *)
 Class SqSubsetEq A := sqsubseteq: relation A.
 Hint Mode SqSubsetEq ! : typeclass_instances.
 Instance: Params (@sqsubseteq) 2.
-- 
GitLab