Adjust comment.

theories/algebra/sets.v

@@ -8,19 +8,21 @@ Set Primitive Projections.
 (** CMRAs for sets with union and disjoint union. *)
 
 (** To define these CMRAs generically without breaking canonical
-structures, we bundle the (mainly) typeclass instances used by the
-CMRAs into canonical structures. These TC instances are defined
-elsewhere, so we keep our `typeclass_instances` hints `Local`.
+structures, we bundle the assumptions made by the CMRAs into canonical
+structures. These assumptions are mainly typeclass instances. These TC
+instances are defined elsewhere, so we keep our `typeclass_instances`
+hints `Local`.
 
 To use these CMRAs with a set implementation, define canonical
 structures for
 
-- [semi_setT] the union CMRA (suffix "U")
+- [semi_setT] assumptions made by the union CMRA (suffix "U")
 
-- [disjoint_setT] the disjoint union CMRA (suffix "D")
+- [disjoint_setT] assumptions made by the disjoint union CMRA (suffix
+  "D")
 
 - [fresh_setT] a "subclass" of [disjoint_setT] with extra assumptions
-  enabling local updates (in the disjoint union CMRA) for allocating
+  enabling, in the disjoint union CMRA, local updates for allocating
   elements not in a finite set (suffix "DF")
 
 The `std++` type [gset], for example, supports all three via [gsetU],