diff --git a/theories/si_logic/bi.v b/theories/si_logic/bi.v
index 7280b9afe232feb088848948ea5faf4201fbbcbc..2efd1b8bfd3405343e73bfd747eddc6261a51484 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -5,6 +5,9 @@ Import siProp_primitive.
 (** BI instances for [siProp], and re-stating the remaining primitive laws in
 terms of the BI interface.  This file does *not* unseal. *)
 
+(** We pick [*] and [-*] to coincide with [∧] and [→], respectively. This seems
+to be the most reasonable choice to fit a "pure" higher-order logic into the
+proofmode's BI framework. *)
 Definition siProp_emp : siProp := siProp_pure True.
 Definition siProp_sep : siProp → siProp → siProp := siProp_and.
 Definition siProp_wand : siProp → siProp → siProp := siProp_impl.
diff --git a/theories/si_logic/siprop.v b/theories/si_logic/siprop.v
index d265fe4171cb60da50c655cbb3c0ee7654b47985..5619e0574abb09a5593da175adad7a58c03da491 100644
--- a/theories/si_logic/siprop.v
+++ b/theories/si_logic/siprop.v
@@ -1,6 +1,9 @@
 From iris.algebra Require Export ofe.
 From iris.bi Require Import notation.
 
+(** The type [siProp] defines "plain" step-indexed propositions, on which we
+define the usual connectives of higher-order logic, and prove that these satisfy
+the usual laws of higher-order logic. *)
 Record siProp := SiProp {
   siProp_holds :> nat → Prop;
   siProp_closed n1 n2 : siProp_holds n1 → n2 ≤ n1 → siProp_holds n2