diff --git a/algebra/cofe.v b/algebra/cofe.v
index 1bfcc66129375181cf34e1efddc4e0b1b3c93810..520ca4f0563c7a54cd7e602b36bba6f866809096 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -613,6 +613,6 @@ Qed.
 (** Notation for writing functors *)
 Notation "∙" := idCF : cFunctor_scope.
 Notation "F1 -n> F2" := (cofe_morCF F1%CF F2%CF) : cFunctor_scope.
-Notation "( F1 , F2 , .. , Fn )" := (prodCF .. (prodCF F1%CF F2%CF) .. Fn%CF) : cFunctor_scope.
+Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
 Notation "â–¶ F"  := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
 Coercion constCF : cofeT >-> cFunctor.