From c079338240561da4fcdabb29a7751e78001ece75 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 10 Feb 2017 12:57:33 +0100
Subject: [PATCH] Hint Mode for LimitPreserving.

---
 theories/algebra/ofe.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1bf21d0e0..9f513eea9 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1073,7 +1073,8 @@ Qed.
 
 (** Sigma *)
 Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop :=
-  limit_preserving : ∀ c : chain A, (∀ n, P (c n)) → P (compl c).
+  limit_preserving (c : chain A) : (∀ n, P (c n)) → P (compl c).
+Hint Mode LimitPreserving + + ! : typeclass_instances.
 
 Section limit_preserving.
   Context {A : ofeT} `{!Cofe A}.
-- 
GitLab