From 829dc99154befb65b9b047e4c1caffb6e1aa6f91 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 19 Feb 2020 16:00:32 +0100
Subject: [PATCH] add comment

---
 theories/coPset.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/coPset.v b/theories/coPset.v
index 09736662..6d092f0d 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
-- 
GitLab