Some comments.

theories/bi/embedding.v

@@ -11,6 +11,7 @@ Typeclasses Opaque embed.
 Hint Mode Embed ! - : typeclass_instances.
 Hint Mode Embed - ! : typeclass_instances.
 
+(* Mixins allow us to create instances easily without having to use Program *)
 Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
   bi_embed_mixin_ne : NonExpansive embed;
   bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) embed;

theories/bi/plainly.v

@@ -8,6 +8,7 @@ Instance: Params (@plainly) 2.
 Notation "■ P" := (plainly P)%I
   (at level 20, right associativity) : bi_scope.
 
+(* Mixins allow us to create instances easily without having to use Program *)
 Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
   bi_plainly_mixin_plainly_ne : NonExpansive plainly;
 

theories/bi/updates.v

@@ -51,6 +51,7 @@ Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I
    format "P  ={ E }▷=∗  Q") : bi_scope.
 
 (** Bundled versions  *)
+(* Mixins allow us to create instances easily without having to use Program *)
 Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
   bi_bupd_mixin_bupd_ne : NonExpansive bupd;
   bi_bupd_mixin_bupd_intro (P : PROP) : P ==∗ P;