From 2a045fd29f10c54940d18eb9f629600c0d5808f4 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Thu, 29 Jul 2021 11:51:09 +0200
Subject: [PATCH] Small tweaks

---
 CHANGELOG.md     | 2 +-
 iris/bi/big_op.v | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b1a338fd5..652673224 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -72,7 +72,7 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Slight change to the `AACC` notation for atomic accessors (which is usually
   only printed, not parsed): added a `,` before `ABORT`, for consistency with `COMM`.
 * Add the lemmas `big_sepM_impl_strong` and `big_sepM_impl_dom_subseteq` that
-  generalize the existing `big_sepM_impl` lemma.
+  generalize the existing `big_sepM_impl` lemma. (by Simon Friis Vindum)
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 104d0be3c..9e82d6e39 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1543,6 +1543,7 @@ Proof.
     rewrite pure_True // left_id // wand_elim_l //.
 Qed.
 
+Lemma big_sepM_impl_dom_subseteq `{Countable K} {A B}
     (Φ : K → A → PROP) (Ψ : K → B → PROP) (m1 : gmap K A) (m2 : gmap K B) :
   dom (gset _) m2 ⊆ dom _ m1 →
   ([∗ map] k↦x ∈ m1, Φ k x) -∗
-- 
GitLab