diff --git a/iris/cmra.v b/iris/cmra.v
index d94b0b1fb7a0b5f13f8fad191ff4d2d78f94b6bb..e4c5589ae4eea4f2797c6c0f7f3d61348d1460fd 100644
--- a/iris/cmra.v
+++ b/iris/cmra.v
@@ -52,6 +52,17 @@ Structure cmraT := CMRAT {
   cmra_extend : CMRAExtend cmra_car
 }.
 Arguments CMRAT _ {_ _ _ _ _ _ _ _ _ _ _}.
+Arguments cmra_car _ : simpl never.
+Arguments cmra_equiv _ _ _ : simpl never.
+Arguments cmra_dist _ _ _ _ : simpl never.
+Arguments cmra_compl _ _ : simpl never.
+Arguments cmra_unit _ _ : simpl never.
+Arguments cmra_op _ _ _ : simpl never.
+Arguments cmra_valid _ _ : simpl never.
+Arguments cmra_validN _ _ _ : simpl never.
+Arguments cmra_included _ _ _ : simpl never.
+Arguments cmra_minus _ _ _ : simpl never.
+Arguments cmra_cmra _ : simpl never.
 Add Printing Constructor cmraT.
 Existing Instances cmra_equiv cmra_dist cmra_compl cmra_unit cmra_op
   cmra_valid cmra_validN cmra_included cmra_minus cmra_cmra cmra_extend.
diff --git a/iris/cmra_maps.v b/iris/cmra_maps.v
index 467f3951bfab3b0842c44377d37522944fbd5d39..68591bece3b6bdabf4ba85c8938218d105dd461d 100644
--- a/iris/cmra_maps.v
+++ b/iris/cmra_maps.v
@@ -138,7 +138,7 @@ Section map.
     * by intros m1 m2 Hm i; rewrite !lookup_fmap; apply included_preserving.
     * by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
   Qed.
-  Local Hint Extern 0 => simpl; apply map_fmap_ne : typeclass_instances.
+  Hint Resolve (map_fmap_ne (M:=M)) : typeclass_instances.
   Definition mapRA_map {A B : cmraT} (f : A -n> B) : mapRA A -n> mapRA B :=
     CofeMor (fmap f : mapRA A → mapRA B).
   Global Instance mapRA_map_ne {A B} n :
diff --git a/iris/cofe.v b/iris/cofe.v
index 38fc2051ab65ceeb705e765980d96b3afe1d99aa..eb43c721c6cc29edf9bd2fd504214e3830e25143 100644
--- a/iris/cofe.v
+++ b/iris/cofe.v
@@ -45,6 +45,11 @@ Structure cofeT := CofeT {
 Arguments CofeT _ {_ _ _ _}.
 Add Printing Constructor cofeT.
 Existing Instances cofe_equiv cofe_dist cofe_compl cofe_cofe.
+Arguments cofe_car _ : simpl never.
+Arguments cofe_equiv _ _ _ : simpl never.
+Arguments cofe_dist _ _ _ _ : simpl never.
+Arguments cofe_compl _ _ : simpl never.
+Arguments cofe_cofe _ : simpl never.
 
 (** General properties *)
 Section cofe.