diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1974baea5df46fcba66a2dd52782428027aee520..5250feeb42858e9a3022202a267e68ba111cd798 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -125,6 +125,7 @@ Class Cofe (A : ofeT) := {
   conv_compl n c : compl c ≡{n}≡ c n;
 }.
 Arguments compl : simpl never.
+Hint Mode Cofe ! : typeclass_instances.
 
 Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c `(NonExpansive f) :
   compl (chain_map f c) ≡ f (compl c).
@@ -264,7 +265,7 @@ Section limit_preserving.
     (∀ x, P x ↔ Q x) → LimitPreserving P → LimitPreserving Q.
   Proof. intros HP Hlimit c ?. apply HP, Hlimit=> n; by apply HP. Qed.
 
-  Global Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _, P).
+  Global Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _ : A, P).
   Proof. intros c HP. apply (HP 0). Qed.
 
   Lemma limit_preserving_discrete (P : A → Prop) :
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 9ba56ac869bec30087823a8331d0136003e9c32e..e1b07ab63f6032f6d81c6813174ba5388c1661fc 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -402,7 +402,7 @@ Lemma entails_lim (cP cQ : chain (uPredO M)) :
   (∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ.
 Proof.
   intros Hlim; split=> n m ? HP.
-  eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl.
+  eapply uPred_holds_ne, Hlim, HP; rewrite ?conv_compl; eauto.
 Qed.
 
 (** Non-expansiveness and setoid morphisms *)