Mode for Unit

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' {

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.