From 6df6c641aadd50cd9808035f77e41048a99e6600 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 May 2020 16:14:49 +0200
Subject: [PATCH] Remove `contractive_ne` and `contractive_proper` as
 instances.

Instead, make them `Hint Immediate` so they are only used at leaves.
---
 theories/algebra/ofe.v | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 71c86a043..5252920af 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -197,6 +197,9 @@ Section ofe.
   Proof. by rewrite -!discrete_iff. Qed.
 End ofe.
 
+Hint Immediate ne_proper : typeclass_instances.
+Hint Immediate ne_proper_2 : typeclass_instances.
+
 (** Contractive functions *)
 Definition dist_later `{Dist A} (n : nat) (x y : A) : Prop :=
   match n with 0 => True | S n => x ≡{n}≡ y end.
@@ -234,12 +237,15 @@ Section contractive.
   Lemma contractive_S n x y : x ≡{n}≡ y → f x ≡{S n}≡ f y.
   Proof. intros. by apply (_ : Contractive f). Qed.
 
-  Global Instance contractive_ne : NonExpansive f | 100.
+  Lemma contractive_ne : NonExpansive f.
   Proof. by intros n x y ?; apply dist_S, contractive_S. Qed.
-  Global Instance contractive_proper : Proper ((≡) ==> (≡)) f | 100.
-  Proof. apply (ne_proper _). Qed.
+  Lemma contractive_proper : Proper ((≡) ==> (≡)) f.
+  Proof. apply ne_proper, contractive_ne. Qed.
 End contractive.
 
+Hint Immediate contractive_ne : typeclass_instances.
+Hint Immediate contractive_proper : typeclass_instances.
+
 Ltac f_contractive :=
   match goal with
   | |- ?f _ ≡{_}≡ ?f _ => simple apply (_ : Proper (dist_later _ ==> _) f)
@@ -798,12 +804,11 @@ Next Obligation.
   apply ofe_morO_map_ne; apply oFunctor_map_ne; split; by apply Hfg.
 Qed.
 Next Obligation.
-  intros F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !oFunctor_map_id.
-  apply (ne_proper f). apply oFunctor_map_id.
+  intros F1 F2 A ? B ? [f ?] ?; simpl. by rewrite /= !oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [h ?] ?; simpl in *.
-  rewrite -!oFunctor_map_compose. do 2 apply (ne_proper _). apply oFunctor_map_compose.
+  by rewrite -!oFunctor_map_compose.
 Qed.
 Notation "F1 -n> F2" := (ofe_morOF F1%OF F2%OF) : oFunctor_scope.
 
-- 
GitLab