diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 9e87934026878d873b99824805952bc4b7c11274..00ab11806f2e78e02ff0437a1ca394ae0b13d191 100644
--- a/theories/bi/embedding.v
+++ b/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;
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 0a553169f3d9abdcc4ff6ca1f4bb817916257ef9..06fff510df79c80d1340fc7d52d23d2ebb68df29 100644
--- a/theories/bi/plainly.v
+++ b/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;
 
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 821f849f65f48333ffc4b94eff2ba76ab131c1ce..cb97dd5e844b843144fb2854eb39c1a27861b0ba 100644
--- a/theories/bi/updates.v
+++ b/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;