diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v index 2b735510d1e850fc24b25a5d2185c0f8194c6197..5dde79ec0062a1db155c08bc5836e40071a0b7a5 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 65dab9152f935aa475f266b435956908ccf95e77..29271bc6e4d63c89cb8f2e1e52f6e4e55e371848 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) := {