From f7b4fa568f3a37b9c977d0fd1d495414a90c49ee Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 13 Aug 2020 11:30:39 +0200
Subject: [PATCH] fix Proof Using warnings

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

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 663f28440..cfa70ab38 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -442,13 +442,11 @@ End fixpointK.
 
 (** Mutual fixpoints *)
 Section fixpointAB.
-  Local Unset Default Proof Using.
-
   Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
   Context (fA : A → B → A).
   Context (fB : A → B → B).
-  Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}.
-  Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB}.
+  Context {fA_contractive : ∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}.
+  Context {fB_contractive : ∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB}.
 
   Local Definition fixpoint_AB (x : A) : B := fixpoint (fB x).
   Local Instance fixpoint_AB_contractive : Contractive fixpoint_AB.
@@ -459,7 +457,7 @@ Section fixpointAB.
 
   Local Definition fixpoint_AA (x : A) : A := fA x (fixpoint_AB x).
   Local Instance fixpoint_AA_contractive : Contractive fixpoint_AA.
-  Proof. solve_contractive. Qed.
+  Proof using fA_contractive. solve_contractive. Qed.
 
   Definition fixpoint_A : A := fixpoint fixpoint_AA.
   Definition fixpoint_B : B := fixpoint_AB fixpoint_A.
@@ -470,11 +468,11 @@ Section fixpointAB.
   Proof. by rewrite {2}/fixpoint_B /fixpoint_AB (fixpoint_unfold _). Qed.
 
   Instance: Proper ((≡) ==> (≡) ==> (≡)) fA.
-  Proof.
+  Proof using fA_contractive.
     apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
   Qed.
   Instance: Proper ((≡) ==> (≡) ==> (≡)) fB.
-  Proof.
+  Proof using fB_contractive.
     apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
   Qed.
 
-- 
GitLab