From 34eefd91027b10f99c930cbc15999fb7175a4168 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 23 Dec 2016 23:55:10 +0100
Subject: [PATCH] Version of [fixpoint_ind] that is easier to use.

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

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index f5da06eeb..6804c1720 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -233,7 +233,7 @@ Section fixpoint.
   Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
 
   Lemma fixpoint_ind (P : A → Prop) :
-    Proper ((≡) ==> iff) P →
+    Proper ((≡) ==> impl) P →
     (∃ x, P x) → (∀ x, P x → P (f x)) →
     (∀ (c : chain A), (∀ n, P (c n)) → P (compl c)) →
     P (fixpoint f).
-- 
GitLab