From 2bf388ccbdd3b5a47a7e18a3b39b9945e47238c2 Mon Sep 17 00:00:00 2001
From: Hai Dang <haidang@mpi-sws.org>
Date: Tue, 20 Apr 2021 07:45:38 +0000
Subject: [PATCH] Apply 2 suggestion(s) to 1 file(s)

---
 theories/fin_maps.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 48aae385..06ef84ef 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1388,7 +1388,7 @@ Section map_filter_misc.
   Proof. apply map_fold_empty. Qed.
 
   Lemma map_filter_singleton i x :
-    P (i,x) → filter P ({[i := x]} : M A) = {[i := x]}.
+    P (i,x) → filter P {[i := x]} =@{M A} {[i := x]}.
   Proof.
     intros ?. rewrite <-insert_empty, map_filter_insert; [|done].
     by rewrite map_filter_empty.
@@ -1438,7 +1438,7 @@ Section map_filter_misc.
 End map_filter_misc.
 
 Lemma map_filter_comm {A}
-  (P : K * A → Prop) `{!∀ x, Decision (P x)} Q `{!∀ x, Decision (Q x)} (m : M A) :
+    (P Q : K * A → Prop) `{!∀ x, Decision (P x), !∀ x, Decision (Q x)} (m : M A) :
   filter P (filter Q m) = filter Q (filter P m).
 Proof. rewrite !map_filter_filter. apply map_filter_ext. naive_solver. Qed.
 
-- 
GitLab