From 71fb10bdce0e06495e60559ea6b73587b3c67619 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 21 Jun 2019 13:09:52 +0200
Subject: [PATCH] Set `Hint Mode` for `Cofe`.

---
 theories/algebra/ofe.v      | 3 ++-
 theories/base_logic/upred.v | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1974baea5..5250feeb4 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 9ba56ac86..e1b07ab63 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 *)
-- 
GitLab