Adapt to Rocq#21180

theories/Algebra/Groups/FreeGroup.v

@@ -241,7 +241,7 @@ Section Reduction.
   (** Finally we have defined the free group on [A] *)
   Definition FreeGroup : Group.
   Proof.
-    snapply (Build_Group freegroup_type); repeat split; exact _.
+    srapply (Build_Group freegroup_type sgop_freegroup); repeat split; exact _.
   Defined.
 
   Definition word_rec (G : Group) (s : A -> G) : A + A -> G.

theories/Algebra/Groups/FreeProduct.v

@@ -524,7 +524,7 @@ Section AmalgamatedFreeProduct.
 
   Definition AmalgamatedFreeProduct : Group.
   Proof.
-    snapply (Build_Group amal_type); repeat split; exact _.
+    snapply (Build_Group amal_type sgop_amal_type); repeat split; exact _.
   Defined.
 
 End AmalgamatedFreeProduct.

theories/Algebra/Groups/Group.v

@@ -969,17 +969,18 @@ Definition grp_prod : Group -> Group -> Group.
 Proof.
   intros G H.
   snapply (Build_Group (G * H)).
-  4: repeat split.
   - intros [g1 h1] [g2 h2].
     exact (g1 * g2, h1 * h2).
   - exact (1, 1).
   - exact (functor_prod inv inv).
-  - exact _.
-  - intros x y z; apply path_prod'; apply simple_associativity.
-  - intros x; apply path_prod'; apply left_identity.
-  - intros x; apply path_prod'; apply right_identity.
-  - intros x; apply path_prod'; apply left_inverse.
-  - intros x; apply path_prod'; apply right_inverse.
+  - split.
+    + repeat split.
+      * exact _.
+      * intros x y z; apply path_prod'; apply simple_associativity.
+      * intros x; apply path_prod'; apply left_identity.
+      * intros x; apply path_prod'; apply right_identity.
+    + intros x; apply path_prod'; apply left_inverse.
+    + intros x; apply path_prod'; apply right_inverse.
 Defined.
 
 (** Maps into the direct product can be built by mapping separately into each factor. *)

theories/Homotopy/HomotopyGroup.v

@@ -46,8 +46,7 @@ Instance is1functor_homotopygroup_type_ptype (n : nat)
   definitionally equal to [Pi 1 (iterated_loops n X)] *)
 Definition Pi1 (X : pType) : Group.
 Proof.
-  srapply (Build_Group (Tr 0 (loops X)));
-    repeat split.
+  srapply (Build_Group (Tr 0 (loops X))).
   (** Operation *)
   - intros x y.
     strip_truncations.
@@ -57,33 +56,35 @@ Proof.
   (** Inverse *)
   - srapply Trunc_rec; intro x.
     exact (tr x^).
-  (** [IsHSet] *)
-  - exact _.
-  (** Associativity *)
-  - intros x y z.
-    strip_truncations.
-    cbn; apply ap.
-    apply concat_p_pp.
-  (** Left identity *)
-  - intro x.
-    strip_truncations.
-    cbn; apply ap.
-    apply concat_1p.
-  (** Right identity *)
-  - intro x.
-    strip_truncations.
-    cbn; apply ap.
-    apply concat_p1.
-  (** Left inverse *)
-  - intro x.
-    strip_truncations.
-    apply (ap tr).
-    apply concat_Vp.
-  (** Right inverse *)
-  - intro x.
-    strip_truncations.
-    apply (ap tr).
-    apply concat_pV.
+  - split.
+    + repeat split.
+      (** [IsHSet] *)
+      * exact _.
+      (** Associativity *)
+      * intros x y z.
+        strip_truncations.
+        cbn; apply ap.
+        apply concat_p_pp.
+      (** Left identity *)
+      * intro x.
+        strip_truncations.
+        cbn; apply ap.
+        apply concat_1p.
+      (** Right identity *)
+      * intro x.
+        strip_truncations.
+        cbn; apply ap.
+        apply concat_p1.
+    (** Left inverse *)
+    + intro x.
+      strip_truncations.
+      apply (ap tr).
+      apply concat_Vp.
+    (** Right inverse *)
+    + intro x.
+      strip_truncations.
+      apply (ap tr).
+      apply concat_pV.
 Defined.
 
 (** Definition of the nth homotopy group *)