From eeb2ebd640da8cf9f56be408d1e1d376a0dce521 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sat, 17 Jul 2021 15:57:59 +0200
Subject: [PATCH] gmap.v: reorder gset instances

---
 theories/gmap.v | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/theories/gmap.v b/theories/gmap.v
index bea67cfd..79813f63 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -237,6 +237,7 @@ Definition gset K `{Countable K} := mapset (gmap K).
 
 Section gset.
   Context `{Countable K}.
+  (* Lift instances of operational TCs from [mapset]. *)
   Global Instance gset_elem_of: ElemOf K (gset K) := _.
   Global Instance gset_empty : Empty (gset K) := _.
   Global Instance gset_singleton : Singleton K (gset K) := _.
@@ -244,10 +245,6 @@ Section gset.
   Global Instance gset_intersection: Intersection (gset K) := _.
   Global Instance gset_difference: Difference (gset K) := _.
   Global Instance gset_elements: Elements K (gset K) := _.
-  Global Instance gset_leibniz : LeibnizEquiv (gset K) := _.
-  Global Instance gset_semi_set : SemiSet K (gset K) | 1 := _.
-  Global Instance gset_set : Set_ K (gset K) | 1 := _.
-  Global Instance gset_fin_set : FinSet K (gset K) := _.
   Global Instance gset_eq_dec : EqDecision (gset K) := _.
   Global Instance gset_countable : Countable (gset K) := _.
   Global Instance gset_equiv_dec : RelDecision (≡@{gset K}) | 1 := _.
@@ -255,6 +252,12 @@ Section gset.
   Global Instance gset_disjoint_dec : RelDecision (##@{gset K}) := _.
   Global Instance gset_subseteq_dec : RelDecision (⊆@{gset K}) := _.
   Global Instance gset_dom {A} : Dom (gmap K A) (gset K) := mapset_dom.
+
+  (* Lift instances of other TCs. *)
+  Global Instance gset_leibniz : LeibnizEquiv (gset K) := _.
+  Global Instance gset_semi_set : SemiSet K (gset K) | 1 := _.
+  Global Instance gset_set : Set_ K (gset K) | 1 := _.
+  Global Instance gset_fin_set : FinSet K (gset K) := _.
   Global Instance gset_dom_spec : FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
   (** If you are looking for a lemma showing that [gset] is extensional, see
-- 
GitLab