From e6ec2867e05184099fbd6b82b04937c4cf182bc4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 29 Nov 2017 13:52:33 +0100
Subject: [PATCH] remove unnecessary side-condition from ofe_funCF_contractive

---
 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 12686722d..d573744c2 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1178,7 +1178,7 @@ Qed.
 
 Notation "T -c> F" := (@ofe_funCF T%type (λ _, F%CF)) : cFunctor_scope.
 
-Instance ofe_funCF_contractive `{Finite C} (F : C → cFunctor) :
+Instance ofe_funCF_contractive {C} (F : C → cFunctor) :
   (∀ c, cFunctorContractive (F c)) → cFunctorContractive (ofe_funCF F).
 Proof.
   intros ? A1 A2 B1 B2 n ?? g.
-- 
GitLab