remove unnecessary side-condition from ofe_funCF_contractive

e6ec2867 · Ralf Jung · 8f1c4c86 · e6ec2867
Commit e6ec2867 authored Nov 29, 2017 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

theories/algebra/ofe.v theories/algebra/ofe.v +1 -1

No files found.
--- 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.