From 1d7cb4154dac72d8d039998a3d54f3d42a58f7db Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 28 May 2021 16:55:20 +0200
Subject: [PATCH] Mode for Unit

---
 iris/algebra/cmra.v         | 5 +++--
 iris_staging/algebra/list.v | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 7824e3ac8..2b735510d 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -181,12 +181,13 @@ Global Instance: Params (@core) 2 := {}.
 
 (** * CMRAs with a unit element *)
 Class Unit (A : Type) := ε : A.
+Global Hint Mode Unit ! : typeclass_instances.
 Global Arguments ε {_ _}.
 
 Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
   mixin_ucmra_unit_valid : ✓ (ε : A);
-  mixin_ucmra_unit_left_id : LeftId (≡) ε (⋅);
-  mixin_ucmra_pcore_unit : pcore ε ≡ Some ε
+  mixin_ucmra_unit_left_id : LeftId (≡@{A}) ε (⋅);
+  mixin_ucmra_pcore_unit : pcore ε ≡@{option A} Some ε
 }.
 
 Structure ucmra := Ucmra' {
diff --git a/iris_staging/algebra/list.v b/iris_staging/algebra/list.v
index b764171fe..36fa11fd2 100644
--- a/iris_staging/algebra/list.v
+++ b/iris_staging/algebra/list.v
@@ -364,7 +364,7 @@ Section properties.
     ✓ x → (l, ε) ~l~> (l ++ [x], {[length l := x]}).
   Proof.
     move => ?.
-    have -> : ({[length l := x]} ≡ {[length l := x]} ⋅ ε) by rewrite right_id.
+    have -> : ({[length l := x]} ≡@{list A} {[length l := x]} ⋅ ε) by rewrite right_id.
     rewrite -list_singletonM_snoc. apply op_local_update => ??.
     rewrite list_singletonM_snoc app_validN cons_validN. split_and? => //; [| constructor].
     by apply cmra_valid_validN.
-- 
GitLab