diff --git a/theories/coPset.v b/theories/coPset.v
index 0973666200bf55f1dcdf2813f74a10ed09e6bfa6..6d092f0d486b0fb1c24c27d58a08487406438be3 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -159,6 +159,7 @@ Instance coPset_singleton : Singleton positive coPset := λ p,
 Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
 Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
 Instance coPset_top : Top coPset := coPLeaf true ↾ I.
+(** Iris and specifically [solve_ndisj] heavily rely on this hint. *)
 Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : core.
 Instance coPset_union : Union coPset := λ X Y,
   let (t1,Ht1) := X in let (t2,Ht2) := Y in