From e0eef94ac040da5f8fea607018ca1e92839bd8ee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 19 Feb 2020 16:13:14 +0100
Subject: [PATCH] Fix compilation after !112 broke it.

---
 theories/coPset.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/coPset.v b/theories/coPset.v
index 6d092f0d..92fb2974 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -159,8 +159,6 @@ 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
   (t1 ∪ t2) ↾ coPset_union_wf _ _ Ht1 Ht2.
@@ -186,6 +184,9 @@ Proof.
   - done.
 Qed.
 
+(** Iris and specifically [solve_ndisj] heavily rely on this hint. *)
+Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : core.
+
 Instance coPset_leibniz : LeibnizEquiv coPset.
 Proof.
   intros X Y; rewrite elem_of_equiv; intros HXY.
-- 
GitLab