From ad376c76b08c5edb596157f617b59b7225b23108 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 22 Jan 2018 10:58:17 +0100
Subject: [PATCH] Update comment.

---
 theories/bi/monpred.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 5b70ef429..51682e881 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.
 
-- 
GitLab