From 6d37f4511cab252ecd557a82f1bc8029dd69f121 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 9 Apr 2018 22:53:52 +0200
Subject: [PATCH] Consistent and higher precedence for default [Equiv]
 instances on maps/collections.

---
 theories/collections.v | 8 +++++---
 theories/fin_maps.v    | 4 +++-
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/theories/collections.v b/theories/collections.v
index 007e95e3..2004d072 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -7,11 +7,13 @@ From stdpp Require Export orders list.
 (* FIXME: This file needs a 'Proof Using' hint, but the default we use
    everywhere makes for lots of extra ssumptions. *)
 
-Instance collection_equiv `{ElemOf A C} : Equiv C := λ X Y,
+(* Higher precedence to make sure these instances are not used for other types
+with an [ElemOf] instance, such as lists. *)
+Instance collection_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
   ∀ x, x ∈ X ↔ x ∈ Y.
-Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
+Instance collection_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
   ∀ x, x ∈ X → x ∈ Y.
-Instance collection_disjoint `{ElemOf A C} : Disjoint C := λ X Y,
+Instance collection_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
   ∀ x, x ∈ X → x ∈ Y → False.
 Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint.
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 121a13ff..d53ea324 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -80,7 +80,9 @@ Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
 Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
   λ f, merge (difference_with f).
 
-Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 18 :=
+(** Higher precedence to make sure it's not used for other types with a [Lookup]
+instance, such as lists. *)
+Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 20 :=
   λ m1 m2, ∀ i, m1 !! i ≡ m2 !! i.
 
 (** The relation [intersection_forall R] on finite maps describes that the
-- 
GitLab