From 3a635ebee09dcf4be0ff9986495e338f43380482 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sun, 1 Sep 2024 18:56:54 +0300 Subject: [PATCH] fix comment in Group.v Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Group.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index c3af650126..2c8bd986a8 100644 --- a/theories/Algebra/Groups/Group.v +++ b/theories/Algebra/Groups/Group.v @@ -88,7 +88,7 @@ End GroupLaws. (** TODO: improve this tactic so that it also rewrites and is able to solve basic group lemmas. *) Tactic Notation "grp_auto" := hnf; intros; eauto with group_db. -(** * Some basic properties of groups *) +(** ** Some basic properties of groups *) (** Groups are pointed sets with point the identity. *) Global Instance ispointed_group (G : Group) @@ -676,7 +676,7 @@ Global Instance is0functor_postcomp_grouphomomorphism {A B C : Group} (h : B $-> : Is0Functor (@cat_postcomp Group _ _ A B C h). Proof. apply Build_Is0Functor. - intros [f ?] [g ?] p a ; exact (ap h (p a)). + intros f g p a ; exact (ap h (p a)). Defined. Global Instance is0functor_precomp_grouphomomorphism