From 9b0f7c75a2387e0ad9fe5d16ec1083a0ece2bea3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Sep 2017 21:36:00 +0200
Subject: [PATCH] Put `Dom` as first argument of `FinMapDom`.

This way, type class search will fail immediately on first type
class constraint of any of the `fin_map_dom` lemmas if no `Dom`
can be found.
---
 theories/fin_map_dom.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 68632ad6..6d50c11a 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -6,10 +6,10 @@ function in a generic way, to allow more efficient implementations. *)
 From stdpp Require Export collections fin_maps.
 Set Default Proof Using "Type*".
 
-Class FinMapDom K M D `{FMap M,
+Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
     ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A),
     OMap M, Merge M, ∀ A, FinMapToList K A (M A), EqDecision K,
-    ∀ A, Dom (M A) D, ElemOf K D, Empty D, Singleton K D,
+    ElemOf K D, Empty D, Singleton K D,
     Union D, Intersection D, Difference D} := {
   finmap_dom_map :>> FinMap K M;
   finmap_dom_collection :>> Collection K D;
-- 
GitLab