From a5ee0c1694b14afcdcb19e2441c1526f15849ead Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 19 Feb 2020 13:32:32 +0100
Subject: [PATCH] move coPset-generic hint to coPset.v

---
 theories/coPset.v     | 1 +
 theories/namespaces.v | 4 ----
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/theories/coPset.v b/theories/coPset.v
index 1b214181..09736662 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.
+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
   (t1 ∪ t2) ↾ coPset_union_wf _ _ Ht1 Ht2.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index 4cd3092d..04f9e931 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -85,10 +85,6 @@ Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.
 Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
 Hint Resolve nclose_subseteq' | 100 : ndisj.
 
-(** Put this hint in [core] so that only only [solve_ndisj], but also [done] and
-friends, can solve trivial goals of the form [E ⊆ ⊤] that occur often. *)
-Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : core.
-
 (** Rules for goals of the form [_ ## _] *)
 (** The base rule that we want to ultimately get down to. *)
 Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
-- 
GitLab