From d1d87f19bfe1c8a5ee38170cdadc606300a7798d Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Mon, 31 May 2021 12:23:18 +0200
Subject: [PATCH] Mode for Dist + CHANGELOG

---
 CHANGELOG.md        | 2 +-
 iris/algebra/cmra.v | 2 +-
 iris/algebra/gmap.v | 2 +-
 iris/algebra/ofe.v  | 1 +
 4 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 607fdf3d9..86a90e100 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -31,7 +31,7 @@ Coq 8.11 is no longer supported in this version of Iris.
   `Dist`, `Op`, `Valid`, `ValidN`, `Unit`, `PCore` now use an `Hint Extern`
   based on `refine` instead of `apply`, in order to use Coq's newer unification
   algorithm.
-* Set `Hint Mode` for the classes `OfeDiscrete`, `Unit`, `CmraMorphism`,
+* Set `Hint Mode` for the classes `OfeDiscrete`, `Dist`, `Unit`, `CmraMorphism`,
   `rFunctorContractive`, `urFunctorContractive`.
 
 **Changes in `bi`:**
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 5dde79ec0..6f73d5d54 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -47,7 +47,7 @@ Section mixin.
     mixin_cmra_op_ne (x : A) : NonExpansive (op x);
     mixin_cmra_pcore_ne n (x y : A) cx :
       x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy;
-    mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
+    mixin_cmra_validN_ne n : Proper (dist (A := A) n ==> impl) (validN n);
     (* valid *)
     mixin_cmra_valid_validN (x : A) : ✓ x ↔ ∀ n, ✓{n} x;
     mixin_cmra_validN_S n (x : A) : ✓{S n} x → ✓{n} x;
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index a61482362..274a3020e 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -66,7 +66,7 @@ Proof.
     [by constructor|by apply lookup_ne].
 Qed.
 Global Instance alter_ne (f : A → A) (k : K) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter f k).
+  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter (M := gmap K A) f k).
 Proof. intros ? m m' Hm k'. by apply partial_alter_ne; [solve_proper|..]. Qed.
 
 Global Instance gmap_empty_discrete : Discrete (∅ : gmap K A).
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 96bf09910..3fe741f8c 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -13,6 +13,7 @@ Set Primitive Projections.
 
 (** Unbundled version *)
 Class Dist A := dist : nat → relation A.
+Global Hint Mode Dist ! : typeclass_instances.
 Global Instance: Params (@dist) 3 := {}.
 Notation "x ≡{ n }≡ y" := (dist n x y)
   (at level 70, n at next level, format "x  ≡{ n }≡  y").
-- 
GitLab