From 329b8c2cad2dbaf6c8f1623aa0acdd7277bddea6 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 27 May 2020 15:13:23 +0200
Subject: [PATCH] Turn local instances ne_proper and ne_proper_2 into lemmas

---
 theories/algebra/ofe.v | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index d73745c2c..71c86a043 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -169,11 +169,15 @@ Section ofe.
   Proof. induction 2; eauto using dist_S. Qed.
   Lemma dist_le' n n' x y : n' ≤ n → x ≡{n}≡ y → x ≡{n'}≡ y.
   Proof. intros; eauto using dist_le. Qed.
-  Instance ne_proper {B : ofeT} (f : A → B) `{!NonExpansive f} :
-    Proper ((≡) ==> (≡)) f | 100.
+  (** [ne_proper] and [ne_proper_2] are not instances to improve efficiency of
+  type class search during setoid rewriting.
+  Instances of [NonExpansive{,2}] are hence accompanied by instances of
+  [Proper] built using these lemmas. *)
+  Lemma ne_proper {B : ofeT} (f : A → B) `{!NonExpansive f} :
+    Proper ((≡) ==> (≡)) f.
   Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
-  Instance ne_proper_2 {B C : ofeT} (f : A → B → C) `{!NonExpansive2 f} :
-    Proper ((≡) ==> (≡) ==> (≡)) f | 100.
+  Lemma ne_proper_2 {B C : ofeT} (f : A → B → C) `{!NonExpansive2 f} :
+    Proper ((≡) ==> (≡) ==> (≡)) f.
   Proof.
      unfold Proper, respectful; setoid_rewrite equiv_dist.
      by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
-- 
GitLab