From 12195779b56bfb5dd0e25b36eba3eeba5c37f8ca Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 26 May 2016 13:00:35 +0200 Subject: [PATCH] Change notation of prod functor to look like a prod instead of a pair. --- algebra/cofe.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/algebra/cofe.v b/algebra/cofe.v index 1bfcc6612..520ca4f05 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. -- GitLab