diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 5b70ef429436439e231652b5ad7c774da3104271..51682e881c7a4dbbd23746276910b8cb5b70e99f 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -11,8 +11,10 @@ Structure biIndex :=
       bi_index_rel_preorder : PreOrder (⊑) }.
 Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
 
-(* TODO : all the use cases of this have a bi_index with a bottom
-   element. Should we add this to the structure? *)
+(* We may want to instantiate monPred with the reflexivity relation in
+   the case where there is no relevent order. In that case, there is
+   no bottom element, so that we do not want to force any BI index to
+   have one. *)
 Class BiIndexBottom {I : biIndex} (bot : I) :=
   bi_index_bot i : bot ⊑ i.