From 994462dc447532ca610ae277c0d4ce95b1dfff6d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 25 May 2022 15:24:01 +0200
Subject: [PATCH] More curry.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index ac26b840..33533c8c 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -176,8 +176,7 @@ and [DK:=gset K]. *)
 Definition map_preimage `{FinMapToList K A MKA, Empty MADK,
     PartialAlter A DK MADK, Empty DK, Singleton K DK, Union DK}
     (m : MKA) : MADK :=
-  map_fold
-    (λ i x, partial_alter (λ mX, Some ({[ i ]} ∪ default ∅ mX)) x) ∅ m.
+  map_fold (λ i, partial_alter (λ mX, Some $ {[ i ]} ∪ default ∅ mX)) ∅ m.
 Typeclasses Opaque map_preimage.
 
 (** * Theorems *)
-- 
GitLab