diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v index 23003d2d212c25304b6b8aab5928bca059589de1..7cb4ce262ec86924642b8bc1bbf768704b890800 100644 --- a/theories/algebra/ofe.v +++ b/theories/algebra/ofe.v @@ -1009,7 +1009,7 @@ Section sigma. Qed. End sigma. -Arguments sigC {A} f. +Arguments sigC {A} P. (** Notation for writing functors *) Notation "∙" := idCF : cFunctor_scope.