From e546ce9ecbba2168eab0688c5778420837a8dad3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 22 Apr 2018 02:48:37 +0200
Subject: [PATCH] actually solve_proper can do this

---
 theories/bi/lib/fixpoint.v | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index 7251c75aa..27dd09a3f 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ -25,10 +25,7 @@ Arguments bi_greatest_fixpoint : simpl never.
 Global Instance least_fixpoint_ne {PROP : bi} {A : ofeT} n :
   Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
           dist n ==> dist n) bi_least_fixpoint.
-Proof.
-  intros F1 F2 HF x1 x2 Hx. rewrite /bi_least_fixpoint /=.
-  do 7 (fast_done || f_equiv). apply HF.
-Qed.
+Proof. solve_proper. Qed.
 
 Section least.
   Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
@@ -87,10 +84,7 @@ Qed.
 Global Instance greatest_fixpoint_ne {PROP : bi} {A : ofeT} n :
   Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
           dist n ==> dist n) bi_greatest_fixpoint.
-Proof.
-  intros F1 F2 HF x1 x2 Hx. rewrite /bi_greatest_fixpoint /=.
-  do 7 (fast_done || f_equiv). apply HF.
-Qed.
+Proof. solve_proper. Qed.
 
 Section greatest.
   Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
-- 
GitLab