From 4adb71a8b47e66984a8671611d226745b93bdfe4 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Mon, 31 May 2021 12:26:28 +0200
Subject: [PATCH] Add remaining modes in cmra.v

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

diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 2b735510d..5dde79ec0 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -251,6 +251,7 @@ Class CmraMorphism {A B : cmra} (f : A → B) := {
   cmra_morphism_pcore x : f <$> pcore x ≡ pcore (f x);
   cmra_morphism_op x y : f (x ⋅ y) ≡ f x ⋅ f y
 }.
+Global Hint Mode CmraMorphism - - ! : typeclass_instances.
 Global Arguments cmra_morphism_validN {_ _} _ {_} _ _ _.
 Global Arguments cmra_morphism_pcore {_ _} _ {_} _.
 Global Arguments cmra_morphism_op {_ _} _ {_} _ _.
@@ -808,6 +809,7 @@ Bind Scope rFunctor_scope with rFunctor.
 Class rFunctorContractive (F : rFunctor) :=
   rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
+Global Hint Mode rFunctorContractive ! : typeclass_instances.
 
 Definition rFunctor_apply (F: rFunctor) (A: ofe) `{!Cofe A} : cmra :=
   rFunctor_car F A A.
@@ -899,6 +901,7 @@ Bind Scope urFunctor_scope with urFunctor.
 Class urFunctorContractive (F : urFunctor) :=
   urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
+Global Hint Mode urFunctorContractive ! : typeclass_instances.
 
 Definition urFunctor_apply (F: urFunctor) (A: ofe) `{!Cofe A} : ucmra :=
   urFunctor_car F A A.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 65dab9152..29271bc6e 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -110,6 +110,7 @@ Global Hint Mode Discrete + ! : typeclass_instances.
 Global Instance: Params (@Discrete) 1 := {}.
 
 Class OfeDiscrete (A : ofe) := ofe_discrete_discrete (x : A) :> Discrete x.
+Global Hint Mode OfeDiscrete ! : typeclass_instances.
 
 (** OFEs with a completion *)
 Record chain (A : ofe) := {
-- 
GitLab