From b3901a5155c1bbf3c76864fae49d59919d86cb8f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Nov 2021 15:29:55 +0100
Subject: [PATCH] Add `Proper` instance for `Dom` on `gmap`.

---
 iris/algebra/gmap.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 7a7c56546..fb96b834f 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -1,5 +1,6 @@
 From stdpp Require Export list gmap.
 From iris.algebra Require Export list cmra.
+From iris.algebra Require Import gset.
 From iris.algebra Require Import updates local_updates proofmode_classes big_op.
 From iris.prelude Require Import options.
 
@@ -94,6 +95,9 @@ Lemma insert_idN n m i x :
   m !! i ≡{n}≡ Some x → <[i:=x]>m ≡{n}≡ m.
 Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
 
+Global Instance gmap_dom_ne n :
+  Proper ((≡{n}@{gmap K A}≡) ==> (=)) (dom (gset K)).
+Proof. intros m1 m2 Hm. apply set_eq=> k. by rewrite !elem_of_dom Hm. Qed.
 End ofe.
 
 Global Instance map_seq_ne {A : ofe} start :
-- 
GitLab