From e386a73811e124ea10ebb742456e048cb0a8c66d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Jan 2021 14:11:23 +0100
Subject: [PATCH] Fix compilation with Coq 8.10 and 8.11.

---
 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 ee7b3562..a7d8d9aa 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1607,7 +1607,7 @@ Proof.
   destruct (Hm k) as [y ->]; [by eauto|]. by f_equal/=.
 Qed.
 
-Lemma map_zip_with_diag {A C} (f : A → A → C) m :
+Lemma map_zip_with_diag {A C} (f : A → A → C) (m : M A) :
   map_zip_with f m m = (λ x, f x x) <$> m.
 Proof.
   unfold map_zip_with. rewrite merge_diag by naive_solver.
-- 
GitLab