From 3ce9cd9aef9736c9daab520af8582825ba3a965d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 3 Mar 2018 11:14:41 +0100
Subject: [PATCH] Some comments.

---
 theories/bi/embedding.v | 1 +
 theories/bi/plainly.v   | 1 +
 theories/bi/updates.v   | 1 +
 3 files changed, 3 insertions(+)

diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 9e8793402..00ab11806 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 0a553169f..06fff510d 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 821f849f6..cb97dd5e8 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;
-- 
GitLab