From aeae16a2dc8c74e7abb5d0406103cf8c1b7fc3e2 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 29 Mar 2019 15:44:42 +0100
Subject: [PATCH] A no-brainer generalization for big_sepM_2_later

---
 theories/bi/big_op.v                     | 5 ++---
 theories/proofmode/class_instances_sbi.v | 4 ++--
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index f2fb0cbd9..7c1c6167e 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1437,9 +1437,8 @@ Section gmap.
 End gmap.
 
 Section gmap2.
-  Context `{Countable K} {A : Type}.
-  Implicit Types m : gmap K A.
-  Implicit Types Φ Ψ : K → A → A → PROP.
+  Context `{Countable K} {A B : Type}.
+  Implicit Types Φ Ψ : K → A → B → PROP.
 
   Lemma big_sepM2_later_1 `{BiAffine PROP} Φ m1 m2 :
     (▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2)
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 22ef7853e..b23e54df1 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -650,8 +650,8 @@ Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opM_commute. by apply big_sepM_mono.
 Qed.
-Global Instance into_laterN_big_sepM2 n `{Countable K} {A}
-    (Φ Ψ : K → A → A → PROP) (m1 m2 : gmap K A) :
+Global Instance into_laterN_big_sepM2 n `{Countable K} {A B}
+    (Φ Ψ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) :
   (∀ x1 x2 k, IntoLaterN false n (Φ k x1 x2) (Ψ k x1 x2)) →
   IntoLaterN false n ([∗ map] k ↦ x1;x2 ∈ m1;m2, Φ k x1 x2) ([∗ map] k ↦ x1;x2 ∈ m1;m2, Ψ k x1 x2).
 Proof.
-- 
GitLab