From 8d0e35d6a507f4c283a47299bc11bc601dec4647 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Fri, 20 Dec 2019 15:26:13 +0100
Subject: [PATCH] fix big_sepM2_fmap and friend to work for keys other than nat

---
 theories/bi/big_op.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index e938f99eb..de8f9c2d3 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1068,7 +1068,7 @@ Section map2.
       naive_solver.
   Qed.
 
-  Lemma big_sepM2_fmap {A' B'} (f : A → A') (g : B → B') (Φ : nat → A' → B' → PROP) m1 m2 :
+  Lemma big_sepM2_fmap {A' B'} (f : A → A') (g : B → B') (Φ : K → A' → B' → PROP) m1 m2 :
     ([∗ map] k↦y1;y2 ∈ f <$> m1; g <$> m2, Φ k y1 y2)
     ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k (f y1) (g y2)).
   Proof.
@@ -1082,12 +1082,12 @@ Section map2.
     - by rewrite big_sepM_fmap.
   Qed.
 
-  Lemma big_sepM2_fmap_l {A'} (f : A → A') (Φ : nat → A' → B → PROP) m1 m2 :
+  Lemma big_sepM2_fmap_l {A'} (f : A → A') (Φ : K → A' → B → PROP) m1 m2 :
     ([∗ map] k↦y1;y2 ∈ f <$> m1; m2, Φ k y1 y2)
     ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k (f y1) y2).
   Proof. rewrite -{1}(map_fmap_id m2). apply big_sepM2_fmap. Qed.
 
-  Lemma big_sepM2_fmap_r {B'} (g : B → B') (Φ : nat → A → B' → PROP) m1 m2 :
+  Lemma big_sepM2_fmap_r {B'} (g : B → B') (Φ : K → A → B' → PROP) m1 m2 :
     ([∗ map] k↦y1;y2 ∈ m1; g <$> m2, Φ k y1 y2)
     ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 (g y2)).
   Proof. rewrite -{1}(map_fmap_id m1). apply big_sepM2_fmap. Qed.
-- 
GitLab