From 29f26e4e8ae75bdcdea5b79c84735cb4483b5224 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 29 Sep 2017 13:49:41 +0200
Subject: [PATCH] Make map_filter only dependent on the typeclasses it actually
 needs.

This fixes the issue of Hai in !6.
---
 theories/fin_maps.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 8fca9913..14fac434 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -130,7 +130,7 @@ is unspecified. *)
 Definition map_fold `{FinMapToList K A M} {B}
   (f : K → A → B → B) (b : B) : M → B := foldr (curry f) b ∘ map_to_list.
 
-Instance map_filter `{FinMap K M} {A} : Filter (K * A) (M A) :=
+Instance map_filter `{FinMapToList K A M, Insert K A M, Empty M} : Filter (K * A) M :=
   λ P _, map_fold (λ k v m, if decide (P (k,v)) then <[k := v]>m else m) ∅.
 
 (** * Theorems *)
-- 
GitLab